:: MSUALG_5 semantic presentation begin definition let X be set ; let R be Relation of X; func EqCl R -> Equivalence_Relation of X means :Def1: :: MSUALG_5:def 1 ( R c= it & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds it c= EqR2 ) ); existence ex b1 being Equivalence_Relation of X st ( R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds b1 c= EqR2 ) ) by EQREL_1:12; uniqueness for b1, b2 being Equivalence_Relation of X st R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds b1 c= EqR2 ) & R c= b2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds b2 c= EqR2 ) holds b1 = b2 proof let C1, C2 be Equivalence_Relation of X; ::_thesis: ( R c= C1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds C1 c= EqR2 ) & R c= C2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds C2 c= EqR2 ) implies C1 = C2 ) assume that A1: R c= C1 and A2: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds C1 c= EqR2 and A3: R c= C2 and A4: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds C2 c= EqR2 ; ::_thesis: C1 = C2 A5: C2 c= C1 by A1, A4; C1 c= C2 by A2, A3; hence C1 = C2 by A5, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def1 defines EqCl MSUALG_5:def_1_:_ for X being set for R being Relation of X for b3 being Equivalence_Relation of X holds ( b3 = EqCl R iff ( R c= b3 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds b3 c= EqR2 ) ) ); theorem Th1: :: MSUALG_5:1 for X being set for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) proof let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) A1: for EqR3 being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR3 holds EqR1 "\/" EqR2 c= EqR3 by EQREL_1:def_2; EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by EQREL_1:def_2; hence EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) by A1, Def1; ::_thesis: verum end; theorem Th2: :: MSUALG_5:2 for X being set for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1 proof let X be set ; ::_thesis: for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1 let EqR1 be Equivalence_Relation of X; ::_thesis: EqCl EqR1 = EqR1 for EqR2 being Equivalence_Relation of X st EqR1 c= EqR2 holds EqR1 c= EqR2 ; hence EqCl EqR1 = EqR1 by Def1; ::_thesis: verum end; begin definition let X be set ; func EqRelLatt X -> strict Lattice means :Def2: :: MSUALG_5:def 2 ( the carrier of it = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of it . (x,y) = x /\ y & the L_join of it . (x,y) = x "\/" y ) ) ); existence ex b1 being strict Lattice st ( the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) ) proof set B = { x where x is Relation of X,X : x is Equivalence_Relation of X } ; id X in { x where x is Relation of X,X : x is Equivalence_Relation of X } ; then reconsider B = { x where x is Relation of X,X : x is Equivalence_Relation of X } as non empty set ; defpred S1[ Element of B, Element of B, Element of B] means ( $1 \/ $2 c= $3 & ( for x9 being Element of B st $1 \/ $2 c= x9 holds $3 c= x9 ) ); A1: for x, y being Element of B ex z being Element of B st S1[x,y,z] proof let x, y be Element of B; ::_thesis: ex z being Element of B st S1[x,y,z] y in B ; then A2: ex y99 being Relation of X,X st ( y = y99 & y99 is Equivalence_Relation of X ) ; x in B ; then ex x99 being Relation of X,X st ( x = x99 & x99 is Equivalence_Relation of X ) ; then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A2; consider z being Equivalence_Relation of X such that A3: x1 \/ y1 c= z and A4: for x9 being Equivalence_Relation of X st x1 \/ y1 c= x9 holds z c= x9 by EQREL_1:12; z in B ; then reconsider z9 = z as Element of B ; take z9 ; ::_thesis: S1[x,y,z9] thus x \/ y c= z9 by A3; ::_thesis: for x9 being Element of B st x \/ y c= x9 holds z9 c= x9 hereby ::_thesis: verum let x9 be Element of B; ::_thesis: ( x \/ y c= x9 implies z9 c= x9 ) assume A5: x \/ y c= x9 ; ::_thesis: z9 c= x9 x9 in B ; then ex x99 being Relation of X,X st ( x9 = x99 & x99 is Equivalence_Relation of X ) ; then reconsider x19 = x9 as Equivalence_Relation of X ; x \/ y c= x19 by A5; hence z9 c= x9 by A4; ::_thesis: verum end; end; consider B1 being BinOp of B such that A6: for x, y being Element of B holds S1[x,y,B1 . (x,y)] from BINOP_1:sch_3(A1); defpred S2[ Element of B, Element of B, Element of B] means $3 = $1 /\ $2; A7: for x, y being Element of B ex z being Element of B st S2[x,y,z] proof let x, y be Element of B; ::_thesis: ex z being Element of B st S2[x,y,z] y in B ; then A8: ex y1 being Relation of X,X st ( y = y1 & y1 is Equivalence_Relation of X ) ; x in B ; then ex x1 being Relation of X,X st ( x = x1 & x1 is Equivalence_Relation of X ) ; then reconsider x9 = x, y9 = y as Equivalence_Relation of X by A8; set z = x9 /\ y9; x9 /\ y9 in B ; then reconsider z = x9 /\ y9 as Element of B ; take z ; ::_thesis: S2[x,y,z] thus S2[x,y,z] ; ::_thesis: verum end; consider B2 being BinOp of B such that A9: for x, y being Element of B holds S2[x,y,B2 . (x,y)] from BINOP_1:sch_3(A7); reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ; A10: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_X_holds_B1_._(x,y)_=_x_"\/"_y let x, y be Equivalence_Relation of X; ::_thesis: B1 . (x,y) = x "\/" y A11: y in B ; x in B ; then reconsider x1 = x, y1 = y as Element of B by A11; reconsider B19 = B1 . (x1,y1) as Element of B ; B19 in B ; then ex B199 being Relation of X,X st ( B19 = B199 & B199 is Equivalence_Relation of X ) ; then reconsider B19 = B19 as Equivalence_Relation of X ; A12: for x9 being Element of B st x1 \/ y1 c= x9 holds B1 . (x1,y1) c= x9 by A6; A13: now__::_thesis:_for_x9_being_Equivalence_Relation_of_X_st_x_\/_y_c=_x9_holds_ B1_._(x,y)_c=_x9 let x9 be Equivalence_Relation of X; ::_thesis: ( x \/ y c= x9 implies B1 . (x,y) c= x9 ) assume A14: x \/ y c= x9 ; ::_thesis: B1 . (x,y) c= x9 x9 in B ; then reconsider x19 = x9 as Element of B ; x \/ y c= x19 by A14; hence B1 . (x,y) c= x9 by A12; ::_thesis: verum end; x1 \/ y1 c= B1 . (x1,y1) by A6; then B19 = x "\/" y by A13, EQREL_1:def_2; hence B1 . (x,y) = x "\/" y ; ::_thesis: verum end; A15: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B1_._(a,(B1_._(b,c)))_=_B1_._((B1_._(a,b)),c) let a, b, c be Element of B; ::_thesis: B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c) b in B ; then A16: ex x2 being Relation of X,X st ( b = x2 & x2 is Equivalence_Relation of X ) ; c in B ; then A17: ex x3 being Relation of X,X st ( c = x3 & x3 is Equivalence_Relation of X ) ; a in B ; then ex x1 being Relation of X,X st ( a = x1 & x1 is Equivalence_Relation of X ) ; then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A16, A17; thus B1 . (a,(B1 . (b,c))) = B1 . (a,(U2 "\/" U3)) by A10 .= U1 "\/" (U2 "\/" U3) by A10 .= (U1 "\/" U2) "\/" U3 by EQREL_1:13 .= B1 . ((U1 "\/" U2),c) by A10 .= B1 . ((B1 . (a,b)),c) by A10 ; ::_thesis: verum end; A18: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider x = a, y = b, z = c as Element of B ; A19: the L_join of L . (a,b) = a "\/" b by LATTICES:def_1; thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def_1 .= B1 . (x,(B1 . (y,z))) by LATTICES:def_1 .= the L_join of L . (( the L_join of L . (a,b)),c) by A15 .= (a "\/" b) "\/" c by A19, LATTICES:def_1 ; ::_thesis: verum end; A20: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B1_._(a,b)_=_B1_._(b,a) let a, b be Element of B; ::_thesis: B1 . (a,b) = B1 . (b,a) b in B ; then A21: ex x2 being Relation of X,X st ( b = x2 & x2 is Equivalence_Relation of X ) ; a in B ; then ex x1 being Relation of X,X st ( a = x1 & x1 is Equivalence_Relation of X ) ; then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A21; thus B1 . (a,b) = U2 "\/" U1 by A10 .= B1 . (b,a) by A10 ; ::_thesis: verum end; A22: for a, b being Element of L holds a "\/" b = b "\/" a proof let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a reconsider x = a, y = b as Element of B ; thus a "\/" b = B1 . (x,y) by LATTICES:def_1 .= the L_join of L . (b,a) by A20 .= b "\/" a by LATTICES:def_1 ; ::_thesis: verum end; A23: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_X_holds_B2_._(x,y)_=_x_/\_y let x, y be Equivalence_Relation of X; ::_thesis: B2 . (x,y) = x /\ y A24: y in B ; x in B ; then reconsider x9 = x, y9 = y as Element of B by A24; B2 . (x9,y9) = x9 /\ y9 by A9; hence B2 . (x,y) = x /\ y ; ::_thesis: verum end; A25: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B2_._(a,(B2_._(b,c)))_=_B2_._((B2_._(a,b)),c) let a, b, c be Element of B; ::_thesis: B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c) b in B ; then A26: ex x2 being Relation of X,X st ( b = x2 & x2 is Equivalence_Relation of X ) ; c in B ; then A27: ex x3 being Relation of X,X st ( c = x3 & x3 is Equivalence_Relation of X ) ; a in B ; then ex x1 being Relation of X,X st ( a = x1 & x1 is Equivalence_Relation of X ) ; then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A26, A27; thus B2 . (a,(B2 . (b,c))) = B2 . (a,(U2 /\ U3)) by A23 .= U1 /\ (U2 /\ U3) by A23 .= (U1 /\ U2) /\ U3 by XBOOLE_1:16 .= B2 . ((U1 /\ U2),c) by A23 .= B2 . ((B2 . (a,b)),c) by A23 ; ::_thesis: verum end; A28: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider x = a, y = b, z = c as Element of B ; A29: the L_meet of L . (a,b) = a "/\" b by LATTICES:def_2; thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def_2 .= B2 . (x,(B2 . (y,z))) by LATTICES:def_2 .= the L_meet of L . (( the L_meet of L . (a,b)),c) by A25 .= (a "/\" b) "/\" c by A29, LATTICES:def_2 ; ::_thesis: verum end; A30: for a, b being Element of L holds a "/\" (a "\/" b) = a proof let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a reconsider x = a, y = b as Element of B ; A31: B2 . (x,(B1 . (x,y))) = x proof y in B ; then A32: ex x2 being Relation of X,X st ( y = x2 & x2 is Equivalence_Relation of X ) ; x in B ; then ex x1 being Relation of X,X st ( x = x1 & x1 is Equivalence_Relation of X ) ; then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A32; B1 . (x,y) = U1 "\/" U2 by A10; hence B2 . (x,(B1 . (x,y))) = U1 /\ (U1 "\/" U2) by A23 .= x by EQREL_1:16 ; ::_thesis: verum end; thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def_2 .= a by A31, LATTICES:def_1 ; ::_thesis: verum end; A33: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B2_._(a,b)_=_B2_._(b,a) let a, b be Element of B; ::_thesis: B2 . (a,b) = B2 . (b,a) b in B ; then A34: ex x2 being Relation of X,X st ( b = x2 & x2 is Equivalence_Relation of X ) ; a in B ; then ex x1 being Relation of X,X st ( a = x1 & x1 is Equivalence_Relation of X ) ; then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A34; thus B2 . (a,b) = U2 /\ U1 by A23 .= B2 . (b,a) by A23 ; ::_thesis: verum end; A35: for a, b being Element of L holds a "/\" b = b "/\" a proof let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a reconsider x = a, y = b as Element of B ; thus a "/\" b = B2 . (x,y) by LATTICES:def_2 .= the L_meet of L . (b,a) by A33 .= b "/\" a by LATTICES:def_2 ; ::_thesis: verum end; for a, b being Element of L holds (a "/\" b) "\/" b = b proof let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b reconsider x = a, y = b as Element of B ; A36: B1 . ((B2 . (x,y)),y) = y proof y in B ; then A37: ex x2 being Relation of X,X st ( y = x2 & x2 is Equivalence_Relation of X ) ; x in B ; then ex x1 being Relation of X,X st ( x = x1 & x1 is Equivalence_Relation of X ) ; then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A37; B2 . (x,y) = U1 /\ U2 by A23; hence B1 . ((B2 . (x,y)),y) = U2 "\/" (U1 /\ U2) by A10 .= y by EQREL_1:17 ; ::_thesis: verum end; thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def_1 .= b by A36, LATTICES:def_2 ; ::_thesis: verum end; then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A22, A18, A35, A28, A30, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; then reconsider L = L as strict Lattice ; take L ; ::_thesis: ( the carrier of L = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) ) ) thus the carrier of L = { x where x is Relation of X,X : x is Equivalence_Relation of X } ; ::_thesis: for x, y being Equivalence_Relation of X holds ( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) thus for x, y being Equivalence_Relation of X holds ( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) by A10, A23; ::_thesis: verum end; uniqueness for b1, b2 being strict Lattice st the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & the carrier of b2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds b1 = b2 proof let P1, P2 be strict Lattice; ::_thesis: ( the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of P1 . (x,y) = x /\ y & the L_join of P1 . (x,y) = x "\/" y ) ) & the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of P2 . (x,y) = x /\ y & the L_join of P2 . (x,y) = x "\/" y ) ) implies P1 = P2 ) assume that A38: the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } and A39: for x, y being Equivalence_Relation of X holds ( the L_meet of P1 . (x,y) = x /\ y & the L_join of P1 . (x,y) = x "\/" y ) and A40: the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } and A41: for x, y being Equivalence_Relation of X holds ( the L_meet of P2 . (x,y) = x /\ y & the L_join of P2 . (x,y) = x "\/" y ) ; ::_thesis: P1 = P2 reconsider Z = the carrier of P1 as non empty set ; now__::_thesis:_for_x,_y_being_Element_of_Z_holds_the_L_meet_of_P1_._(x,y)_=_the_L_meet_of_P2_._(x,y) let x, y be Element of Z; ::_thesis: the L_meet of P1 . (x,y) = the L_meet of P2 . (x,y) y in Z ; then A42: ex x3 being Relation of X,X st ( y = x3 & x3 is Equivalence_Relation of X ) by A38; x in Z ; then ex x2 being Relation of X,X st ( x = x2 & x2 is Equivalence_Relation of X ) by A38; then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A42; thus the L_meet of P1 . (x,y) = x1 /\ y1 by A39 .= the L_meet of P2 . (x,y) by A41 ; ::_thesis: verum end; then A43: the L_meet of P1 = the L_meet of P2 by A38, A40, BINOP_1:2; now__::_thesis:_for_x,_y_being_Element_of_Z_holds_the_L_join_of_P1_._(x,y)_=_the_L_join_of_P2_._(x,y) let x, y be Element of Z; ::_thesis: the L_join of P1 . (x,y) = the L_join of P2 . (x,y) y in Z ; then A44: ex x3 being Relation of X,X st ( y = x3 & x3 is Equivalence_Relation of X ) by A38; x in Z ; then ex x2 being Relation of X,X st ( x = x2 & x2 is Equivalence_Relation of X ) by A38; then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A44; thus the L_join of P1 . (x,y) = x1 "\/" y1 by A39 .= the L_join of P2 . (x,y) by A41 ; ::_thesis: verum end; hence P1 = P2 by A38, A40, A43, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines EqRelLatt MSUALG_5:def_2_:_ for X being set for b2 being strict Lattice holds ( b2 = EqRelLatt X iff ( the carrier of b2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds ( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) ) ); begin registration let I be set ; let M be ManySortedSet of I; cluster Relation-like I -defined Function-like total V95() MSEquivalence_Relation-like for ManySortedRelation of M,M; existence ex b1 being ManySortedRelation of M st b1 is MSEquivalence_Relation-like proof deffunc H1( set ) -> Element of bool [:(M . I),(M . I):] = id (M . I); consider f being ManySortedSet of I such that A1: for d being set st d in I holds f . d = H1(d) from PBOOLE:sch_4(); for i being set st i in I holds f . i is Relation of (M . i),(M . i) proof let i be set ; ::_thesis: ( i in I implies f . i is Relation of (M . i),(M . i) ) assume i in I ; ::_thesis: f . i is Relation of (M . i),(M . i) then f . i = id (M . i) by A1; hence f . i is Relation of (M . i),(M . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedRelation of M by MSUALG_4:def_1; take f ; ::_thesis: f is MSEquivalence_Relation-like for i being set for R being Relation of (M . i) st i in I & f . i = R holds R is Equivalence_Relation of (M . i) proof let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & f . i = R holds R is Equivalence_Relation of (M . i) let R be Relation of (M . i); ::_thesis: ( i in I & f . i = R implies R is Equivalence_Relation of (M . i) ) assume that A2: i in I and A3: f . i = R ; ::_thesis: R is Equivalence_Relation of (M . i) R = id (M . i) by A1, A2, A3; hence R is Equivalence_Relation of (M . i) ; ::_thesis: verum end; hence f is MSEquivalence_Relation-like by MSUALG_4:def_2; ::_thesis: verum end; end; definition let I be set ; let M be ManySortedSet of I; mode Equivalence_Relation of M is MSEquivalence_Relation-like ManySortedRelation of M; end; definition let I be non empty set ; let M be ManySortedSet of I; let R be ManySortedRelation of M; func EqCl R -> Equivalence_Relation of M means :Def3: :: MSUALG_5:def 3 for i being Element of I holds it . i = EqCl (R . i); existence ex b1 being Equivalence_Relation of M st for i being Element of I holds b1 . i = EqCl (R . i) proof deffunc H1( Element of I) -> Equivalence_Relation of (M . $1) = EqCl (R . $1); consider EqR being ManySortedSet of I such that A1: for i being Element of I holds EqR . i = H1(i) from PBOOLE:sch_5(); for i being set st i in I holds EqR . i is Relation of (M . i) proof let i be set ; ::_thesis: ( i in I implies EqR . i is Relation of (M . i) ) assume i in I ; ::_thesis: EqR . i is Relation of (M . i) then reconsider i9 = i as Element of I ; EqR . i = EqCl (R . i9) by A1; hence EqR . i is Relation of (M . i) ; ::_thesis: verum end; then reconsider EqR = EqR as ManySortedRelation of M by MSUALG_4:def_1; for i being set for R being Relation of (M . i) st i in I & EqR . i = R holds R is Equivalence_Relation of (M . i) proof let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & EqR . i = R holds R is Equivalence_Relation of (M . i) let R1 be Relation of (M . i); ::_thesis: ( i in I & EqR . i = R1 implies R1 is Equivalence_Relation of (M . i) ) assume that A2: i in I and A3: EqR . i = R1 ; ::_thesis: R1 is Equivalence_Relation of (M . i) reconsider i9 = i as Element of I by A2; R1 = EqCl (R . i9) by A1, A3; hence R1 is Equivalence_Relation of (M . i) ; ::_thesis: verum end; then reconsider EqR = EqR as Equivalence_Relation of M by MSUALG_4:def_2; take EqR ; ::_thesis: for i being Element of I holds EqR . i = EqCl (R . i) thus for i being Element of I holds EqR . i = EqCl (R . i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Equivalence_Relation of M st ( for i being Element of I holds b1 . i = EqCl (R . i) ) & ( for i being Element of I holds b2 . i = EqCl (R . i) ) holds b1 = b2 proof let C1, C2 be Equivalence_Relation of M; ::_thesis: ( ( for i being Element of I holds C1 . i = EqCl (R . i) ) & ( for i being Element of I holds C2 . i = EqCl (R . i) ) implies C1 = C2 ) assume that A4: for i being Element of I holds C1 . i = EqCl (R . i) and A5: for i being Element of I holds C2 . i = EqCl (R . i) ; ::_thesis: C1 = C2 now__::_thesis:_for_i_being_set_st_i_in_I_holds_ C1_._i_=_C2_._i let i be set ; ::_thesis: ( i in I implies C1 . i = C2 . i ) assume i in I ; ::_thesis: C1 . i = C2 . i then reconsider i1 = i as Element of I ; thus C1 . i = EqCl (R . i1) by A4 .= C2 . i by A5 ; ::_thesis: verum end; hence C1 = C2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def3 defines EqCl MSUALG_5:def_3_:_ for I being non empty set for M being ManySortedSet of I for R being ManySortedRelation of M for b4 being Equivalence_Relation of M holds ( b4 = EqCl R iff for i being Element of I holds b4 . i = EqCl (R . i) ); theorem :: MSUALG_5:3 for I being non empty set for M being ManySortedSet of I for EqR being Equivalence_Relation of M holds EqCl EqR = EqR proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR being Equivalence_Relation of M holds EqCl EqR = EqR let M be ManySortedSet of I; ::_thesis: for EqR being Equivalence_Relation of M holds EqCl EqR = EqR let EqR be Equivalence_Relation of M; ::_thesis: EqCl EqR = EqR now__::_thesis:_for_i_being_Element_of_I_holds_EqR_._i_=_EqCl_(EqR_._i) let i be Element of I; ::_thesis: EqR . i = EqCl (EqR . i) reconsider ER = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def_2; thus EqR . i = EqCl ER by Th2 .= EqCl (EqR . i) ; ::_thesis: verum end; hence EqCl EqR = EqR by Def3; ::_thesis: verum end; begin definition let I be non empty set ; let M be ManySortedSet of I; let EqR1, EqR2 be Equivalence_Relation of M; funcEqR1 "\/" EqR2 -> Equivalence_Relation of M means :Def4: :: MSUALG_5:def 4 ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & it = EqCl EqR3 ); existence ex b1 being Equivalence_Relation of M ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) proof deffunc H1( set ) -> set = (EqR1 \/ EqR2) . $1; consider E being ManySortedSet of I such that A1: for i being set st i in I holds E . i = H1(i) from PBOOLE:sch_4(); for i being set st i in I holds E . i is Relation of (M . i) proof let i be set ; ::_thesis: ( i in I implies E . i is Relation of (M . i) ) assume A2: i in I ; ::_thesis: E . i is Relation of (M . i) then reconsider i9 = i as Element of I ; E . i = (EqR1 \/ EqR2) . i by A1, A2 .= (EqR1 . i9) \/ (EqR2 . i9) by PBOOLE:def_4 ; hence E . i is Relation of (M . i) ; ::_thesis: verum end; then reconsider E = E as ManySortedRelation of M by MSUALG_4:def_1; take EqCl E ; ::_thesis: ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & EqCl E = EqCl EqR3 ) take E ; ::_thesis: ( E = EqR1 \/ EqR2 & EqCl E = EqCl E ) thus ( E = EqR1 \/ EqR2 & EqCl E = EqCl E ) by A1, PBOOLE:3; ::_thesis: verum end; uniqueness for b1, b2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) & ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & b2 = EqCl EqR3 ) holds b1 = b2 ; commutativity for b1, EqR1, EqR2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) holds ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR2 \/ EqR1 & b1 = EqCl EqR3 ) ; end; :: deftheorem Def4 defines "\/" MSUALG_5:def_4_:_ for I being non empty set for M being ManySortedSet of I for EqR1, EqR2, b5 being Equivalence_Relation of M holds ( b5 = EqR1 "\/" EqR2 iff ex EqR3 being ManySortedRelation of M st ( EqR3 = EqR1 \/ EqR2 & b5 = EqCl EqR3 ) ); theorem Th4: :: MSUALG_5:4 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2 proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2 let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2 let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 consider EqR3 being ManySortedRelation of M such that A1: EqR3 = EqR1 \/ EqR2 and A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ EqR3_._i_c=_(EqR1_"\/"_EqR2)_._i let i be set ; ::_thesis: ( i in I implies EqR3 . i c= (EqR1 "\/" EqR2) . i ) assume i in I ; ::_thesis: EqR3 . i c= (EqR1 "\/" EqR2) . i then reconsider i9 = i as Element of I ; EqR3 . i c= EqCl (EqR3 . i9) by Def1; hence EqR3 . i c= (EqR1 "\/" EqR2) . i by A2, Def3; ::_thesis: verum end; hence EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by A1, PBOOLE:def_2; ::_thesis: verum end; theorem Th5: :: MSUALG_5:5 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR1 "\/" EqR2 c= EqR proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR1 "\/" EqR2 c= EqR let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR1 "\/" EqR2 c= EqR let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR1 "\/" EqR2 c= EqR consider EqR3 being ManySortedRelation of M such that A1: EqR3 = EqR1 \/ EqR2 and A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4; let EqR be Equivalence_Relation of M; ::_thesis: ( EqR1 \/ EqR2 c= EqR implies EqR1 "\/" EqR2 c= EqR ) assume A3: EqR1 \/ EqR2 c= EqR ; ::_thesis: EqR1 "\/" EqR2 c= EqR now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (EqR1_"\/"_EqR2)_._i_c=_EqR_._i let i be set ; ::_thesis: ( i in I implies (EqR1 "\/" EqR2) . i c= EqR . i ) assume A4: i in I ; ::_thesis: (EqR1 "\/" EqR2) . i c= EqR . i then reconsider i9 = i as Element of I ; EqR . i9 is Relation of (M . i) ; then reconsider E = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def_2; EqR3 . i c= E by A3, A1, A4, PBOOLE:def_2; then EqCl (EqR3 . i9) c= E by Def1; hence (EqR1 "\/" EqR2) . i c= EqR . i by A2, Def3; ::_thesis: verum end; hence EqR1 "\/" EqR2 c= EqR by PBOOLE:def_2; ::_thesis: verum end; theorem Th6: :: MSUALG_5:6 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR3 c= EqR ) holds EqR3 = EqR1 "\/" EqR2 proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR3 c= EqR ) holds EqR3 = EqR1 "\/" EqR2 let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR3 c= EqR ) holds EqR3 = EqR1 "\/" EqR2 let EqR1, EqR2, EqR3 be Equivalence_Relation of M; ::_thesis: ( EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2 ) assume that A1: EqR1 \/ EqR2 c= EqR3 and A2: for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds EqR3 c= EqR ; ::_thesis: EqR3 = EqR1 "\/" EqR2 A3: EqR1 "\/" EqR2 c= EqR3 by A1, Th5; EqR3 c= EqR1 "\/" EqR2 by A2, Th4; hence EqR3 = EqR1 "\/" EqR2 by A3, PBOOLE:146; ::_thesis: verum end; theorem :: MSUALG_5:7 for I being non empty set for M being ManySortedSet of I for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR let M be ManySortedSet of I; ::_thesis: for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR let EqR be Equivalence_Relation of M; ::_thesis: EqR "\/" EqR = EqR for EqR3 being Equivalence_Relation of M st EqR \/ EqR c= EqR3 holds EqR c= EqR3 ; hence EqR "\/" EqR = EqR by Th6; ::_thesis: verum end; theorem Th8: :: MSUALG_5:8 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) let EqR1, EqR2, EqR3 be Equivalence_Relation of M; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) for EqR4 being Equivalence_Relation of M st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 proof let EqR4 be Equivalence_Relation of M; ::_thesis: ( EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 ) A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Th4; assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 then A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Th4; EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:14; then EqR2 "\/" EqR3 c= EqR4 by A2, PBOOLE:13; then A3: EqR2 \/ EqR3 c= EqR4 by A1, PBOOLE:13; EqR2 c= EqR2 \/ EqR3 by PBOOLE:14; then A4: EqR2 c= EqR4 by A3, PBOOLE:13; EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:14; then EqR1 c= EqR4 by A2, PBOOLE:13; then EqR1 \/ EqR2 c= EqR4 by A4, PBOOLE:16; then A5: EqR1 "\/" EqR2 c= EqR4 by Th5; EqR3 c= EqR2 \/ EqR3 by PBOOLE:14; then EqR3 c= EqR4 by A3, PBOOLE:13; then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5, PBOOLE:16; hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Th5; ::_thesis: verum end; then A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3) ; for EqR4 being Equivalence_Relation of M st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 proof let EqR4 be Equivalence_Relation of M; ::_thesis: ( EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 ) A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th4; assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; ::_thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 then A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Th4; EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:14; then EqR1 "\/" EqR2 c= EqR4 by A8, PBOOLE:13; then A9: EqR1 \/ EqR2 c= EqR4 by A7, PBOOLE:13; EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:14; then A10: EqR3 c= EqR4 by A8, PBOOLE:13; EqR2 c= EqR1 \/ EqR2 by PBOOLE:14; then EqR2 c= EqR4 by A9, PBOOLE:13; then EqR2 \/ EqR3 c= EqR4 by A10, PBOOLE:16; then A11: EqR2 "\/" EqR3 c= EqR4 by Th5; EqR1 c= EqR1 \/ EqR2 by PBOOLE:14; then EqR1 c= EqR4 by A9, PBOOLE:13; then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11, PBOOLE:16; hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Th5; ::_thesis: verum end; then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3 ; hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6, PBOOLE:146; ::_thesis: verum end; theorem Th9: :: MSUALG_5:9 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1 proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1 let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1 let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: EqR1 /\ (EqR1 "\/" EqR2) = EqR1 A1: EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by PBOOLE:15; A2: EqR1 c= EqR1 \/ EqR2 by PBOOLE:14; EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th4; then EqR1 c= EqR1 "\/" EqR2 by A2, PBOOLE:13; then EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by PBOOLE:17; hence EqR1 /\ (EqR1 "\/" EqR2) = EqR1 by A1, PBOOLE:146; ::_thesis: verum end; theorem Th10: :: MSUALG_5:10 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds EqR1 "\/" EqR = EqR1 proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds EqR1 "\/" EqR = EqR1 let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds EqR1 "\/" EqR = EqR1 let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: for EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds EqR1 "\/" EqR = EqR1 A1: EqR1 = EqR1 \/ (EqR1 /\ EqR2) by PBOOLE:31; A2: for EqR4 being Equivalence_Relation of M st EqR1 \/ (EqR1 /\ EqR2) c= EqR4 holds EqR1 c= EqR4 by PBOOLE:31; let EqR be Equivalence_Relation of M; ::_thesis: ( EqR = EqR1 /\ EqR2 implies EqR1 "\/" EqR = EqR1 ) assume EqR = EqR1 /\ EqR2 ; ::_thesis: EqR1 "\/" EqR = EqR1 hence EqR1 "\/" EqR = EqR1 by A1, A2, Th6; ::_thesis: verum end; theorem Th11: :: MSUALG_5:11 for I being non empty set for M being ManySortedSet of I for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: EqR1 /\ EqR2 is Equivalence_Relation of M for i being set st i in I holds (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i) proof let i be set ; ::_thesis: ( i in I implies (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i) ) assume A1: i in I ; ::_thesis: (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i) then reconsider U19 = EqR1 . i as Relation of (M . i),(M . i) by MSUALG_4:def_1; reconsider U29 = EqR2 . i as Relation of (M . i),(M . i) by A1, MSUALG_4:def_1; (EqR1 /\ EqR2) . i = U19 /\ U29 by A1, PBOOLE:def_5; hence (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i) ; ::_thesis: verum end; then reconsider U3 = EqR1 /\ EqR2 as ManySortedRelation of M by MSUALG_4:def_1; for i being set for R being Relation of (M . i) st i in I & U3 . i = R holds R is Equivalence_Relation of (M . i) proof let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & U3 . i = R holds R is Equivalence_Relation of (M . i) let R be Relation of (M . i); ::_thesis: ( i in I & U3 . i = R implies R is Equivalence_Relation of (M . i) ) assume that A2: i in I and A3: U3 . i = R ; ::_thesis: R is Equivalence_Relation of (M . i) reconsider U29 = EqR2 . i as Relation of (M . i) by A2, MSUALG_4:def_1; reconsider U29 = U29 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def_2; reconsider U19 = EqR1 . i as Relation of (M . i) by A2, MSUALG_4:def_1; reconsider U19 = U19 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def_2; U19 /\ U29 is Equivalence_Relation of (M . i) ; hence R is Equivalence_Relation of (M . i) by A2, A3, PBOOLE:def_5; ::_thesis: verum end; hence EqR1 /\ EqR2 is Equivalence_Relation of M by MSUALG_4:def_2; ::_thesis: verum end; definition let I be non empty set ; let M be ManySortedSet of I; func EqRelLatt M -> strict Lattice means :Def5: :: MSUALG_5:def 5 ( ( for x being set holds ( x in the carrier of it iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of it . (x,y) = x /\ y & the L_join of it . (x,y) = x "\/" y ) ) ); existence ex b1 being strict Lattice st ( ( for x being set holds ( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) ) proof set f = the Equivalence_Relation of M; defpred S1[ set ] means $1 is Equivalence_Relation of M; deffunc H1( Element of I) -> set = bool [:(M . $1),(M . $1):]; consider M2 being ManySortedSet of I such that A1: for i being Element of I holds M2 . i = H1(i) from PBOOLE:sch_5(); consider B being set such that A2: for x being set holds ( x in B iff ( x in product M2 & S1[x] ) ) from XBOOLE_0:sch_1(); A3: for EqR being Equivalence_Relation of M holds EqR in product M2 proof let EqR be Equivalence_Relation of M; ::_thesis: EqR in product M2 A4: for x being set st x in dom M2 holds EqR . x in M2 . x proof let x be set ; ::_thesis: ( x in dom M2 implies EqR . x in M2 . x ) assume x in dom M2 ; ::_thesis: EqR . x in M2 . x then reconsider x9 = x as Element of I ; A5: EqR . x9 is Subset of [:(M . x9),(M . x9):] ; M2 . x9 = bool [:(M . x9),(M . x9):] by A1; hence EqR . x in M2 . x by A5; ::_thesis: verum end; dom EqR = I by PARTFUN1:def_2 .= dom M2 by PARTFUN1:def_2 ; hence EqR in product M2 by A4, CARD_3:9; ::_thesis: verum end; then the Equivalence_Relation of M in product M2 ; then reconsider B = B as non empty set by A2; defpred S2[ Element of B, Element of B, Element of B] means for x1, y1 being Equivalence_Relation of M st x1 = $1 & y1 = $2 holds ex EqR3 being ManySortedRelation of M st ( EqR3 = x1 \/ y1 & $3 = EqCl EqR3 ); A6: for x, y being Element of B ex z being Element of B st S2[x,y,z] proof let x, y be Element of B; ::_thesis: ex z being Element of B st S2[x,y,z] reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2; set z = x9 "\/" y9; x9 "\/" y9 in product M2 by A3; then reconsider z = x9 "\/" y9 as Element of B by A2; take z ; ::_thesis: S2[x,y,z] let x1, y1 be Equivalence_Relation of M; ::_thesis: ( x1 = x & y1 = y implies ex EqR3 being ManySortedRelation of M st ( EqR3 = x1 \/ y1 & z = EqCl EqR3 ) ) assume that A7: x1 = x and A8: y1 = y ; ::_thesis: ex EqR3 being ManySortedRelation of M st ( EqR3 = x1 \/ y1 & z = EqCl EqR3 ) thus ex EqR3 being ManySortedRelation of M st ( EqR3 = x1 \/ y1 & z = EqCl EqR3 ) by A7, A8, Def4; ::_thesis: verum end; consider B1 being BinOp of B such that A9: for x, y being Element of B holds S2[x,y,B1 . (x,y)] from BINOP_1:sch_3(A6); defpred S3[ Element of B, Element of B, Element of B] means for x1, y1 being Equivalence_Relation of M st x1 = $1 & y1 = $2 holds $3 = x1 /\ y1; A10: for x, y being Element of B ex z being Element of B st S3[x,y,z] proof let x, y be Element of B; ::_thesis: ex z being Element of B st S3[x,y,z] reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2; set z = x9 /\ y9; for i being set st i in I holds (x9 /\ y9) . i is Relation of (M . i) proof let i be set ; ::_thesis: ( i in I implies (x9 /\ y9) . i is Relation of (M . i) ) assume i in I ; ::_thesis: (x9 /\ y9) . i is Relation of (M . i) then reconsider i9 = i as Element of I ; (x9 /\ y9) . i = (x9 . i9) /\ (y9 . i9) by PBOOLE:def_5; hence (x9 /\ y9) . i is Relation of (M . i) ; ::_thesis: verum end; then reconsider z = x9 /\ y9 as ManySortedRelation of M by MSUALG_4:def_1; for i being set for R being Relation of (M . i) st i in I & z . i = R holds R is Equivalence_Relation of (M . i) proof let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & z . i = R holds R is Equivalence_Relation of (M . i) let R be Relation of (M . i); ::_thesis: ( i in I & z . i = R implies R is Equivalence_Relation of (M . i) ) assume that A11: i in I and A12: z . i = R ; ::_thesis: R is Equivalence_Relation of (M . i) reconsider i9 = i as Element of I by A11; reconsider x199 = x9 . i9, y199 = y9 . i9 as Relation of (M . i) ; reconsider x99 = x199, y99 = y199 as Equivalence_Relation of (M . i) by MSUALG_4:def_2; R = x99 /\ y99 by A12, PBOOLE:def_5; hence R is Equivalence_Relation of (M . i) ; ::_thesis: verum end; then reconsider z = z as Equivalence_Relation of M by MSUALG_4:def_2; z in product M2 by A3; then reconsider z = z as Element of B by A2; take z ; ::_thesis: S3[x,y,z] thus S3[x,y,z] ; ::_thesis: verum end; consider B2 being BinOp of B such that A13: for x, y being Element of B holds S3[x,y,B2 . (x,y)] from BINOP_1:sch_3(A10); reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ; A14: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_M_holds_B1_._(x,y)_=_x_"\/"_y let x, y be Equivalence_Relation of M; ::_thesis: B1 . (x,y) = x "\/" y A15: y in product M2 by A3; x in product M2 by A3; then reconsider x9 = x, y9 = y as Element of B by A2, A15; ex EqR3 being ManySortedRelation of M st ( EqR3 = x \/ y & B1 . (x9,y9) = EqCl EqR3 ) by A9; hence B1 . (x,y) = x "\/" y by Def4; ::_thesis: verum end; A16: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B1_._(a,(B1_._(b,c)))_=_B1_._((B1_._(a,b)),c) let a, b, c be Element of B; ::_thesis: B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c) reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2; thus B1 . (a,(B1 . (b,c))) = B1 . (a,(U2 "\/" U3)) by A14 .= U1 "\/" (U2 "\/" U3) by A14 .= (U1 "\/" U2) "\/" U3 by Th8 .= B1 . ((U1 "\/" U2),c) by A14 .= B1 . ((B1 . (a,b)),c) by A14 ; ::_thesis: verum end; A17: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider x = a, y = b, z = c as Element of B ; A18: the L_join of L . (a,b) = a "\/" b by LATTICES:def_1; thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def_1 .= B1 . (x,(B1 . (y,z))) by LATTICES:def_1 .= the L_join of L . (( the L_join of L . (a,b)),c) by A16 .= (a "\/" b) "\/" c by A18, LATTICES:def_1 ; ::_thesis: verum end; A19: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_M_holds_B2_._(x,y)_=_x_/\_y let x, y be Equivalence_Relation of M; ::_thesis: B2 . (x,y) = x /\ y A20: y in product M2 by A3; x in product M2 by A3; then reconsider x9 = x, y9 = y as Element of B by A2, A20; A21: y9 = y ; x9 = x ; hence B2 . (x,y) = x /\ y by A13, A21; ::_thesis: verum end; A22: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B2_._(a,(B2_._(b,c)))_=_B2_._((B2_._(a,b)),c) let a, b, c be Element of B; ::_thesis: B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c) reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2; reconsider EQR1 = U2 /\ U3 as Equivalence_Relation of M by Th11; reconsider EQR2 = U1 /\ U2 as Equivalence_Relation of M by Th11; thus B2 . (a,(B2 . (b,c))) = B2 . (a,EQR1) by A19 .= U1 /\ (U2 /\ U3) by A19 .= (U1 /\ U2) /\ U3 by PBOOLE:29 .= B2 . (EQR2,c) by A19 .= B2 . ((B2 . (a,b)),c) by A19 ; ::_thesis: verum end; A23: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider x = a, y = b, z = c as Element of B ; A24: the L_meet of L . (a,b) = a "/\" b by LATTICES:def_2; thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def_2 .= B2 . (x,(B2 . (y,z))) by LATTICES:def_2 .= the L_meet of L . (( the L_meet of L . (a,b)),c) by A22 .= (a "/\" b) "/\" c by A24, LATTICES:def_2 ; ::_thesis: verum end; A25: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B1_._(a,b)_=_B1_._(b,a) let a, b be Element of B; ::_thesis: B1 . (a,b) = B1 . (b,a) reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2; thus B1 . (a,b) = U1 "\/" U2 by A14 .= B1 . (b,a) by A14 ; ::_thesis: verum end; A26: for a, b being Element of L holds a "\/" b = b "\/" a proof let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a reconsider x = a, y = b as Element of B ; thus a "\/" b = B1 . (x,y) by LATTICES:def_1 .= the L_join of L . (b,a) by A25 .= b "\/" a by LATTICES:def_1 ; ::_thesis: verum end; A27: for a, b being Element of L holds (a "/\" b) "\/" b = b proof let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b reconsider x = a, y = b as Element of B ; A28: B1 . ((B2 . (x,y)),y) = y proof reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2; reconsider EQR = U1 /\ U2 as Equivalence_Relation of M by Th11; B2 . (x,y) = U1 /\ U2 by A19; hence B1 . ((B2 . (x,y)),y) = EQR "\/" U2 by A14 .= y by Th10 ; ::_thesis: verum end; thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def_1 .= b by A28, LATTICES:def_2 ; ::_thesis: verum end; A29: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B2_._(a,b)_=_B2_._(b,a) let a, b be Element of B; ::_thesis: B2 . (a,b) = B2 . (b,a) reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2; thus B2 . (a,b) = U2 /\ U1 by A19 .= B2 . (b,a) by A19 ; ::_thesis: verum end; A30: for a, b being Element of L holds a "/\" b = b "/\" a proof let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a reconsider x = a, y = b as Element of B ; thus a "/\" b = B2 . (x,y) by LATTICES:def_2 .= the L_meet of L . (b,a) by A29 .= b "/\" a by LATTICES:def_2 ; ::_thesis: verum end; for a, b being Element of L holds a "/\" (a "\/" b) = a proof let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a reconsider x = a, y = b as Element of B ; A31: B2 . (x,(B1 . (x,y))) = x proof reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2; B1 . (x,y) = U1 "\/" U2 by A14; hence B2 . (x,(B1 . (x,y))) = U1 /\ (U1 "\/" U2) by A19 .= x by Th9 ; ::_thesis: verum end; thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def_2 .= a by A31, LATTICES:def_1 ; ::_thesis: verum end; then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A26, A17, A27, A30, A23, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; then reconsider L = L as strict Lattice ; take L ; ::_thesis: ( ( for x being set holds ( x in the carrier of L iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) ) ) thus for x being set holds ( x in the carrier of L iff x is Equivalence_Relation of M ) ::_thesis: for x, y being Equivalence_Relation of M holds ( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) proof let x be set ; ::_thesis: ( x in the carrier of L iff x is Equivalence_Relation of M ) thus ( x in the carrier of L implies x is Equivalence_Relation of M ) by A2; ::_thesis: ( x is Equivalence_Relation of M implies x in the carrier of L ) thus ( x is Equivalence_Relation of M implies x in the carrier of L ) ::_thesis: verum proof assume A32: x is Equivalence_Relation of M ; ::_thesis: x in the carrier of L then x in product M2 by A3; hence x in the carrier of L by A2, A32; ::_thesis: verum end; end; thus for x, y being Equivalence_Relation of M holds ( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) by A14, A19; ::_thesis: verum end; uniqueness for b1, b2 being strict Lattice st ( for x being set holds ( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & ( for x being set holds ( x in the carrier of b2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds b1 = b2 proof let S1, S2 be strict Lattice; ::_thesis: ( ( for x being set holds ( x in the carrier of S1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of S1 . (x,y) = x /\ y & the L_join of S1 . (x,y) = x "\/" y ) ) & ( for x being set holds ( x in the carrier of S2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of S2 . (x,y) = x /\ y & the L_join of S2 . (x,y) = x "\/" y ) ) implies S1 = S2 ) assume that A33: for x being set holds ( x in the carrier of S1 iff x is Equivalence_Relation of M ) and A34: for x, y being Equivalence_Relation of M holds ( the L_meet of S1 . (x,y) = x /\ y & the L_join of S1 . (x,y) = x "\/" y ) and A35: for x being set holds ( x in the carrier of S2 iff x is Equivalence_Relation of M ) and A36: for x, y being Equivalence_Relation of M holds ( the L_meet of S2 . (x,y) = x /\ y & the L_join of S2 . (x,y) = x "\/" y ) ; ::_thesis: S1 = S2 reconsider Z = the carrier of S1 as non empty set ; now__::_thesis:_for_x_being_set_holds_ (_x_in_the_carrier_of_S1_iff_x_in_the_carrier_of_S2_) let x be set ; ::_thesis: ( x in the carrier of S1 iff x in the carrier of S2 ) ( x is Equivalence_Relation of M iff x in the carrier of S2 ) by A35; hence ( x in the carrier of S1 iff x in the carrier of S2 ) by A33; ::_thesis: verum end; then A37: the carrier of S1 = the carrier of S2 by TARSKI:1; A38: now__::_thesis:_for_x,_y_being_Element_of_Z_holds_ (_the_L_meet_of_S1_._(x,y)_=_the_L_meet_of_S2_._(x,y)_&_the_L_join_of_S1_._(x,y)_=_the_L_join_of_S2_._(x,y)_) let x, y be Element of Z; ::_thesis: ( the L_meet of S1 . (x,y) = the L_meet of S2 . (x,y) & the L_join of S1 . (x,y) = the L_join of S2 . (x,y) ) reconsider x1 = x, y1 = y as Equivalence_Relation of M by A33; thus the L_meet of S1 . (x,y) = x1 /\ y1 by A34 .= the L_meet of S2 . (x,y) by A36 ; ::_thesis: the L_join of S1 . (x,y) = the L_join of S2 . (x,y) thus the L_join of S1 . (x,y) = x1 "\/" y1 by A34 .= the L_join of S2 . (x,y) by A36 ; ::_thesis: verum end; then the L_meet of S1 = the L_meet of S2 by A37, BINOP_1:2; hence S1 = S2 by A37, A38, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines EqRelLatt MSUALG_5:def_5_:_ for I being non empty set for M being ManySortedSet of I for b3 being strict Lattice holds ( b3 = EqRelLatt M iff ( ( for x being set holds ( x in the carrier of b3 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds ( the L_meet of b3 . (x,y) = x /\ y & the L_join of b3 . (x,y) = x "\/" y ) ) ) ); begin registration let S be non empty ManySortedSign ; let A be MSAlgebra over S; cluster MSEquivalence-like -> MSEquivalence_Relation-like for ManySortedRelation of the Sorts of A, the Sorts of A; coherence for b1 being ManySortedRelation of A st b1 is MSEquivalence-like holds b1 is MSEquivalence_Relation-like by MSUALG_4:def_3; end; theorem Th12: :: MSUALG_5:12 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for o being OperSymbol of S for C1, C2 being MSCongruence of A for x1, y1 being set for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for o being OperSymbol of S for C1, C2 being MSCongruence of A for x1, y1 being set for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S for C1, C2 being MSCongruence of A for x1, y1 being set for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) let o be OperSymbol of S; ::_thesis: for C1, C2 being MSCongruence of A for x1, y1 being set for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) let C1, C2 be MSCongruence of A; ::_thesis: for x1, y1 being set for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) let x1, y1 be set ; ::_thesis: for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) let a1, b1 be FinSequence; ::_thesis: ( [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) implies for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) assume A1: [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) ; ::_thesis: for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) let x, y be Element of Args (o,A); ::_thesis: ( x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) assume that A2: x = (a1 ^ <*x1*>) ^ b1 and A3: y = (a1 ^ <*y1*>) ^ b1 ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) A4: y = a1 ^ (<*y1*> ^ b1) by A3, FINSEQ_1:32; A5: x = a1 ^ (<*x1*> ^ b1) by A2, FINSEQ_1:32; now__::_thesis:_[((Den_(o,A))_._x),((Den_(o,A))_._y)]_in_(C1_._(the_result_sort_of_o))_\/_(C2_._(the_result_sort_of_o)) percases ( [x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1)) or [x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1)) ) by A1, XBOOLE_0:def_3; supposeA6: [x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1)) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) for n being Nat st n in dom x holds [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) proof let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) ) assume A7: n in dom x ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) then reconsider dz = dom (the_arity_of o) as non empty set by MSUALG_3:6; A8: n in dom (the_arity_of o) by A7, MSUALG_3:6; then A9: n in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def_2; reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ; A10: not product so is empty ; pi ((Args (o,A)),n) = pi (((( the Sorts of A #) * the Arity of S) . o),n) by MSUALG_1:def_4 .= pi ((( the Sorts of A #) . ( the Arity of S . o)),n) by FUNCT_2:15 .= pi ((( the Sorts of A #) . (the_arity_of o)),n) by MSUALG_1:def_1 .= pi ((product ( the Sorts of A * (the_arity_of o))),n) by FINSEQ_2:def_5 .= ( the Sorts of A * (the_arity_of o)) . n by A9, A10, CARD_3:12 .= the Sorts of A . ((the_arity_of o) . n) by A8, FUNCT_1:13 .= the Sorts of A . ((the_arity_of o) /. n) by A8, PARTFUN1:def_6 ; then A11: x . n in the Sorts of A . ((the_arity_of o) /. n) by CARD_3:def_6; A12: ( n in dom (a1 ^ <*x1*>) or ex k being Nat st ( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A2, A7, FINSEQ_1:25; now__::_thesis:_[(x_._n),(y_._n)]_in_C1_._((the_arity_of_o)_/._n) percases ( n in dom a1 or ex m being Nat st ( m in dom <*x1*> & n = (len a1) + m ) or ex k being Element of NAT st ( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A12, FINSEQ_1:25; supposeA13: n in dom a1 ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) then A14: y . n = a1 . n by A4, FINSEQ_1:def_7; x . n = a1 . n by A5, A13, FINSEQ_1:def_7; hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by A11, A14, EQREL_1:5; ::_thesis: verum end; suppose ex m being Nat st ( m in dom <*x1*> & n = (len a1) + m ) ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) then consider m being Nat such that A15: m in dom <*x1*> and A16: n = (len a1) + m ; A17: m in Seg 1 by A15, FINSEQ_1:38; then A18: m = 1 by FINSEQ_1:2, TARSKI:def_1; then A19: n in Seg ((len a1) + 1) by A16, FINSEQ_1:4; then n in Seg ((len a1) + (len <*y1*>)) by FINSEQ_1:40; then n in Seg (len (a1 ^ <*y1*>)) by FINSEQ_1:22; then n in dom (a1 ^ <*y1*>) by FINSEQ_1:def_3; then A20: y . n = (a1 ^ <*y1*>) . ((len a1) + 1) by A3, A16, A18, FINSEQ_1:def_7 .= y1 by FINSEQ_1:42 ; n in Seg ((len a1) + (len <*x1*>)) by A19, FINSEQ_1:40; then n in Seg (len (a1 ^ <*x1*>)) by FINSEQ_1:22; then n in dom (a1 ^ <*x1*>) by FINSEQ_1:def_3; then x . n = (a1 ^ <*x1*>) . ((len a1) + 1) by A2, A16, A18, FINSEQ_1:def_7 .= x1 by FINSEQ_1:42 ; hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by A6, A16, A17, A20, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; suppose ex k being Element of NAT st ( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) then consider k being Element of NAT such that A21: k in dom b1 and A22: n = (len (a1 ^ <*x1*>)) + k ; n = ((len a1) + (len <*x1*>)) + k by A22, FINSEQ_1:22; then n = ((len a1) + 1) + k by FINSEQ_1:40; then n = ((len a1) + (len <*y1*>)) + k by FINSEQ_1:40; then n = (len (a1 ^ <*y1*>)) + k by FINSEQ_1:22; then A23: y . n = b1 . k by A3, A21, FINSEQ_1:def_7; x . n = b1 . k by A2, A21, A22, FINSEQ_1:def_7; hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by A11, A23, EQREL_1:5; ::_thesis: verum end; end; end; hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) ; ::_thesis: verum end; then [((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o) by MSUALG_4:def_4; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA24: [x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1)) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) for n being Nat st n in dom x holds [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) proof let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) ) assume A25: n in dom x ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) then reconsider dz = dom (the_arity_of o) as non empty set by MSUALG_3:6; A26: n in dom (the_arity_of o) by A25, MSUALG_3:6; then A27: n in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def_2; reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ; A28: not product so is empty ; pi ((Args (o,A)),n) = pi (((( the Sorts of A #) * the Arity of S) . o),n) by MSUALG_1:def_4 .= pi ((( the Sorts of A #) . ( the Arity of S . o)),n) by FUNCT_2:15 .= pi ((( the Sorts of A #) . (the_arity_of o)),n) by MSUALG_1:def_1 .= pi ((product ( the Sorts of A * (the_arity_of o))),n) by FINSEQ_2:def_5 .= ( the Sorts of A * (the_arity_of o)) . n by A27, A28, CARD_3:12 .= the Sorts of A . ((the_arity_of o) . n) by A26, FUNCT_1:13 .= the Sorts of A . ((the_arity_of o) /. n) by A26, PARTFUN1:def_6 ; then A29: x . n in the Sorts of A . ((the_arity_of o) /. n) by CARD_3:def_6; A30: ( n in dom (a1 ^ <*x1*>) or ex k being Nat st ( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A2, A25, FINSEQ_1:25; now__::_thesis:_[(x_._n),(y_._n)]_in_C2_._((the_arity_of_o)_/._n) percases ( n in dom a1 or ex m being Nat st ( m in dom <*x1*> & n = (len a1) + m ) or ex k being Element of NAT st ( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A30, FINSEQ_1:25; supposeA31: n in dom a1 ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) then A32: y . n = a1 . n by A4, FINSEQ_1:def_7; x . n = a1 . n by A5, A31, FINSEQ_1:def_7; hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by A29, A32, EQREL_1:5; ::_thesis: verum end; suppose ex m being Nat st ( m in dom <*x1*> & n = (len a1) + m ) ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) then consider m being Nat such that A33: m in dom <*x1*> and A34: n = (len a1) + m ; A35: m in Seg 1 by A33, FINSEQ_1:38; then A36: m = 1 by FINSEQ_1:2, TARSKI:def_1; then A37: n in Seg ((len a1) + 1) by A34, FINSEQ_1:4; then n in Seg ((len a1) + (len <*y1*>)) by FINSEQ_1:40; then n in Seg (len (a1 ^ <*y1*>)) by FINSEQ_1:22; then n in dom (a1 ^ <*y1*>) by FINSEQ_1:def_3; then A38: y . n = (a1 ^ <*y1*>) . ((len a1) + 1) by A3, A34, A36, FINSEQ_1:def_7 .= y1 by FINSEQ_1:42 ; n in Seg ((len a1) + (len <*x1*>)) by A37, FINSEQ_1:40; then n in Seg (len (a1 ^ <*x1*>)) by FINSEQ_1:22; then n in dom (a1 ^ <*x1*>) by FINSEQ_1:def_3; then x . n = (a1 ^ <*x1*>) . ((len a1) + 1) by A2, A34, A36, FINSEQ_1:def_7 .= x1 by FINSEQ_1:42 ; hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by A24, A34, A35, A38, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; suppose ex k being Element of NAT st ( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) then consider k being Element of NAT such that A39: k in dom b1 and A40: n = (len (a1 ^ <*x1*>)) + k ; n = ((len a1) + (len <*x1*>)) + k by A40, FINSEQ_1:22; then n = ((len a1) + 1) + k by FINSEQ_1:40; then n = ((len a1) + (len <*y1*>)) + k by FINSEQ_1:40; then n = (len (a1 ^ <*y1*>)) + k by FINSEQ_1:22; then A41: y . n = b1 . k by A3, A39, FINSEQ_1:def_7; x . n = b1 . k by A2, A39, A40, FINSEQ_1:def_7; hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by A29, A41, EQREL_1:5; ::_thesis: verum end; end; end; hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) ; ::_thesis: verum end; then [((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o) by MSUALG_4:def_4; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ; ::_thesis: verum end; theorem Th13: :: MSUALG_5:13 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for o being OperSymbol of S for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for o being OperSymbol of S for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let o be OperSymbol of S; ::_thesis: for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let C1, C2 be MSCongruence of A; ::_thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let C be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( C = C1 "\/" C2 implies for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) ) assume A1: C = C1 "\/" C2 ; ::_thesis: for x1, y1 being set for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) consider C9 being ManySortedRelation of the Sorts of A such that A2: C9 = C1 \/ C2 and A3: C1 "\/" C2 = EqCl C9 by Def4; A4: (C1 . (the_result_sort_of o)) "\/" (C2 . (the_result_sort_of o)) = EqCl ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) by Th1 .= EqCl (C9 . (the_result_sort_of o)) by A2, PBOOLE:def_4 .= (C1 "\/" C2) . (the_result_sort_of o) by A3, Def3 ; consider D9 being ManySortedRelation of the Sorts of A such that A5: D9 = C1 \/ C2 and A6: C1 "\/" C2 = EqCl D9 by Def4; let x1, y1 be set ; ::_thesis: for n being Element of NAT for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let n be Element of NAT ; ::_thesis: for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let a1, a2, b1 be FinSequence; ::_thesis: ( len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) implies for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) ) assume that A7: len a1 = n and A8: len a1 = len a2 and A9: for k being Element of NAT st k in dom a1 holds [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ; ::_thesis: ( not [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) or not [x1,y1] in C . ((the_arity_of o) /. (n + 1)) or for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) ) A10: (C1 . ((the_arity_of o) /. (n + 1))) "\/" (C2 . ((the_arity_of o) /. (n + 1))) = EqCl ((C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1)))) by Th1 .= EqCl (D9 . ((the_arity_of o) /. (n + 1))) by A5, PBOOLE:def_4 .= (C1 "\/" C2) . ((the_arity_of o) /. (n + 1)) by A6, Def3 ; set y = (a2 ^ <*y1*>) ^ b1; assume that A11: [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) and A12: [x1,y1] in C . ((the_arity_of o) /. (n + 1)) ; ::_thesis: for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) let x be Element of Args (o,A); ::_thesis: ( x = (a1 ^ <*x1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) ) assume A13: x = (a1 ^ <*x1*>) ^ b1 ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) A14: the Sorts of A . (the_result_sort_of o) = the Sorts of A . ( the ResultSort of S . o) by MSUALG_1:def_2 .= ( the Sorts of A * the ResultSort of S) . o by FUNCT_2:15 .= Result (o,A) by MSUALG_1:def_5 ; then (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ; then consider p being FinSequence such that A15: 1 <= len p and A16: (Den (o,A)) . ((a1 ^ <*x1*>) ^ b1) = p . 1 and A17: (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) = p . (len p) and A18: for i being Element of NAT st 1 <= i & i < len p holds [(p . i),(p . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A1, A11, A13, A4, EQREL_1:28; x1 in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A12, ZFMISC_1:87; then consider f being FinSequence such that A19: 1 <= len f and A20: x1 = f . 1 and A21: y1 = f . (len f) and A22: for i being Element of NAT st 1 <= i & i < len f holds [(f . i),(f . (i + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A1, A12, A10, EQREL_1:28; deffunc H1( Nat) -> set = (Den (o,A)) . ((a2 ^ <*(f . $1)*>) ^ b1); consider g being FinSequence such that A23: ( len g = len f & ( for i being Nat st i in dom g holds g . i = H1(i) ) ) from FINSEQ_1:sch_2(); A24: dom g = Seg (len f) by A23, FINSEQ_1:def_3; A25: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def_3 .= Seg (len (a1 ^ (<*x1*> ^ b1))) by FINSEQ_1:32 .= Seg ((len a2) + (len (<*x1*> ^ b1))) by A8, FINSEQ_1:22 .= Seg (len (a2 ^ (<*x1*> ^ b1))) by FINSEQ_1:22 .= Seg (len ((a2 ^ <*x1*>) ^ b1)) by FINSEQ_1:32 .= dom ((a2 ^ <*x1*>) ^ b1) by FINSEQ_1:def_3 ; ex q being FinSequence st ( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) ) proof take q = p ^ g; ::_thesis: ( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) ) A26: len q = (len p) + (len g) by FINSEQ_1:22; hence 1 <= len q by A15, NAT_1:12; ::_thesis: ( (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) ) 1 in dom p by A15, FINSEQ_3:25; hence q . 1 = (Den (o,A)) . x by A13, A16, FINSEQ_1:def_7; ::_thesis: ( (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) ) A27: len g in Seg (len f) by A19, A23, FINSEQ_1:1; then len g in dom g by A23, FINSEQ_1:def_3; hence q . (len q) = g . (len g) by A26, FINSEQ_1:def_7 .= (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) by A21, A23, A24, A27 ; ::_thesis: for i being Element of NAT st 1 <= i & i < len q holds [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) A28: len p <> 0 by A15; hereby ::_thesis: verum let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len q implies [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) assume that A29: 1 <= i and A30: i < len q ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) A31: ( ( 1 <= i & i < len p ) or ( (len p) + 1 <= i & i < len q ) or i = len p ) proof assume that A32: ( not 1 <= i or not i < len p ) and A33: ( not (len p) + 1 <= i or not i < len q ) ; ::_thesis: i = len p i <= len p by A30, A33, NAT_1:13; hence i = len p by A29, A32, XXREAL_0:1; ::_thesis: verum end; A34: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def_3 .= dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; A35: len ((a2 ^ <*x1*>) ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32 .= (len a2) + (len (<*x1*> ^ b1)) by FINSEQ_1:22 .= len (a1 ^ (<*x1*> ^ b1)) by A8, FINSEQ_1:22 .= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:32 .= len (the_arity_of o) by A34, FINSEQ_1:6 ; A36: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_x_holds_ x_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k) let k be Element of NAT ; ::_thesis: ( k in dom x implies x . k in the Sorts of A . ((the_arity_of o) /. k) ) assume k in dom x ; ::_thesis: x . k in the Sorts of A . ((the_arity_of o) /. k) then A37: k in Seg (len (the_arity_of o)) by A25, A35, FINSEQ_1:def_3; then A38: k in dom (the_arity_of o) by FINSEQ_1:def_3; then A39: k in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def_2; reconsider dz = dom (the_arity_of o) as non empty set by A37, FINSEQ_1:def_3; reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ; A40: not product so is empty ; pi ((Args (o,A)),k) = pi (((( the Sorts of A #) * the Arity of S) . o),k) by MSUALG_1:def_4 .= pi ((( the Sorts of A #) . ( the Arity of S . o)),k) by FUNCT_2:15 .= pi ((( the Sorts of A #) . (the_arity_of o)),k) by MSUALG_1:def_1 .= pi ((product ( the Sorts of A * (the_arity_of o))),k) by FINSEQ_2:def_5 .= ( the Sorts of A * (the_arity_of o)) . k by A39, A40, CARD_3:12 .= the Sorts of A . ((the_arity_of o) . k) by A38, FUNCT_1:13 .= the Sorts of A . ((the_arity_of o) /. k) by A38, PARTFUN1:def_6 ; hence x . k in the Sorts of A . ((the_arity_of o) /. k) by CARD_3:def_6; ::_thesis: verum end; A41: ex i1 being Nat st len p = i1 + 1 by A28, NAT_1:6; now__::_thesis:_[(q_._i),(q_._(i_+_1))]_in_(C1_._(the_result_sort_of_o))_\/_(C2_._(the_result_sort_of_o)) percases ( ( 1 <= i & i < len p ) or i = len p or ( (len p) + 1 <= i & i < len q ) ) by A31; supposeA42: ( 1 <= i & i < len p ) ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) then A43: i + 1 <= len p by NAT_1:13; 1 <= i + 1 by A42, NAT_1:13; then i + 1 in dom p by A43, FINSEQ_3:25; then A44: q . (i + 1) = p . (i + 1) by FINSEQ_1:def_7; i in dom p by A42, FINSEQ_3:25; then q . i = p . i by FINSEQ_1:def_7; hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A18, A42, A44; ::_thesis: verum end; supposeA45: i = len p ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) then i in Seg (len p) by A41, FINSEQ_1:4; then i in dom p by FINSEQ_1:def_3; then A46: q . i = (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A17, A45, FINSEQ_1:def_7; A47: 1 in Seg (len g) by A19, A23, FINSEQ_1:1; then 1 in dom g by FINSEQ_1:def_3; then A48: q . (i + 1) = g . 1 by A45, FINSEQ_1:def_7 .= (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A20, A23, A24, A47 ; for k being Nat st k in dom ((a2 ^ <*x1*>) ^ b1) holds ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) proof let k be Nat; ::_thesis: ( k in dom ((a2 ^ <*x1*>) ^ b1) implies ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ) assume A50: k in dom ((a2 ^ <*x1*>) ^ b1) ; ::_thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then A51: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32; now__::_thesis:_((a2_^_<*x1*>)_^_b1)_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k) percases ( k in dom a2 or ex n1 being Nat st ( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ) by A51, FINSEQ_1:25; supposeA52: k in dom a2 ; ::_thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then k in Seg (len a2) by FINSEQ_1:def_3; then k in dom a1 by A8, FINSEQ_1:def_3; then A53: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9; ((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32 .= a2 . k by A52, FINSEQ_1:def_7 ; hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A53, ZFMISC_1:87; ::_thesis: verum end; suppose ex n1 being Nat st ( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ; ::_thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then consider n1 being Nat such that A54: n1 in dom (<*x1*> ^ b1) and A55: k = (len a2) + n1 ; ((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32 .= (<*x1*> ^ b1) . n1 by A54, A55, FINSEQ_1:def_7 .= (a1 ^ (<*x1*> ^ b1)) . k by A8, A54, A55, FINSEQ_1:def_7 .= x . k by A13, FINSEQ_1:32 ; hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A25, A36, A50; ::_thesis: verum end; end; end; hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum end; then reconsider de = (a2 ^ <*x1*>) ^ b1 as Element of Args (o,A) by A35, MSAFREE2:5; A56: field (C2 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9; field (C1 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9; then field ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) = ( the Sorts of A . (the_result_sort_of o)) \/ ( the Sorts of A . (the_result_sort_of o)) by A56, RELAT_1:18 .= the Sorts of A . (the_result_sort_of o) ; then A57: (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def_9; (Den (o,A)) . de in the Sorts of A . (the_result_sort_of o) by A14; hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A46, A48, A57, RELAT_2:def_1; ::_thesis: verum end; supposeA58: ( (len p) + 1 <= i & i < len q ) ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) then len p < i by NAT_1:13; then reconsider j = i - (len p) as Element of NAT by NAT_1:21; A59: 1 <= j + 1 by NAT_1:12; len f = (len q) - (len p) by A23, A26, XCMPLX_1:26; then A60: j < len f by A58, XREAL_1:9; then j + 1 <= len f by NAT_1:13; then j + 1 in Seg (len f) by A59, FINSEQ_1:1; then A61: (i + 1) - (len p) in Seg (len f) by XCMPLX_1:29; A62: 1 <= j by A58, XREAL_1:19; then A63: [(f . j),(f . (j + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A60; then A64: f . ((i - (len p)) + 1) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by ZFMISC_1:87; A65: for k being Nat st k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) holds ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) proof let k be Nat; ::_thesis: ( k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ) assume A66: k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then A67: ( k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) or ex n1 being Nat st ( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by FINSEQ_1:25; now__::_thesis:_((a2_^_<*(f_._((i_+_1)_-_(len_p)))*>)_^_b1)_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k) percases ( k in dom a2 or ex n2 being Nat st ( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st ( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by A67, FINSEQ_1:25; supposeA68: k in dom a2 ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then k in Seg (len a2) by FINSEQ_1:def_3; then k in dom a1 by A8, FINSEQ_1:def_3; then A69: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9; ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . ((i + 1) - (len p)))*> ^ b1)) . k by FINSEQ_1:32 .= a2 . k by A68, FINSEQ_1:def_7 ; hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A69, ZFMISC_1:87; ::_thesis: verum end; suppose ex n2 being Nat st ( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then consider n2 being Nat such that A70: n2 in dom <*(f . ((i + 1) - (len p)))*> and A71: k = (len a2) + n2 ; n2 in Seg 1 by A70, FINSEQ_1:38; then A72: k = (len a1) + 1 by A8, A71, FINSEQ_1:2, TARSKI:def_1; then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4; then k in Seg ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:40; then k in Seg (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:22; then k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:def_3; then ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . ((i + 1) - (len p)))*>) . k by FINSEQ_1:def_7 .= f . ((i + 1) - (len p)) by A8, A72, FINSEQ_1:42 ; hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A64, A72, XCMPLX_1:29; ::_thesis: verum end; supposeA73: ex n1 being Element of NAT st ( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) A74: len (a1 ^ <*x1*>) = (len a1) + (len <*x1*>) by FINSEQ_1:22 .= (len a2) + 1 by A8, FINSEQ_1:40 .= (len a2) + (len <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:40 .= len (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:22 ; A75: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def_3 .= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22 .= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22 .= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40 .= Seg (((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:40 .= Seg ((len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:22 .= Seg (len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1)) by FINSEQ_1:22 .= dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) by FINSEQ_1:def_3 ; consider n1 being Element of NAT such that A76: n1 in dom b1 and A77: k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 by A73; ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = b1 . n1 by A76, A77, FINSEQ_1:def_7 .= x . k by A13, A76, A77, A74, FINSEQ_1:def_7 ; hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A66, A75; ::_thesis: verum end; end; end; hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum end; A78: f . (i - (len p)) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A63, ZFMISC_1:87; A79: for k being Nat st k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) holds ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) proof let k be Nat; ::_thesis: ( k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ) assume A80: k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then A81: ( k in dom (a2 ^ <*(f . (i - (len p)))*>) or ex n1 being Nat st ( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by FINSEQ_1:25; now__::_thesis:_((a2_^_<*(f_._(i_-_(len_p)))*>)_^_b1)_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k) percases ( k in dom a2 or ex n2 being Nat st ( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st ( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by A81, FINSEQ_1:25; supposeA82: k in dom a2 ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then k in Seg (len a2) by FINSEQ_1:def_3; then k in dom a1 by A8, FINSEQ_1:def_3; then A83: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9; ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . (i - (len p)))*> ^ b1)) . k by FINSEQ_1:32 .= a2 . k by A82, FINSEQ_1:def_7 ; hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A83, ZFMISC_1:87; ::_thesis: verum end; suppose ex n2 being Nat st ( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) then consider n2 being Nat such that A84: n2 in dom <*(f . (i - (len p)))*> and A85: k = (len a2) + n2 ; A86: n2 in Seg 1 by A84, FINSEQ_1:38; then A87: k = (len a1) + 1 by A8, A85, FINSEQ_1:2, TARSKI:def_1; then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4; then k in Seg ((len a2) + (len <*(f . (i - (len p)))*>)) by FINSEQ_1:40; then k in Seg (len (a2 ^ <*(f . (i - (len p)))*>)) by FINSEQ_1:22; then k in dom (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:def_3; then ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . (i - (len p)))*>) . k by FINSEQ_1:def_7 .= f . (i - (len p)) by A8, A87, FINSEQ_1:42 ; hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A8, A78, A85, A86, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; supposeA88: ex n1 being Element of NAT st ( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) A89: len (a1 ^ <*x1*>) = (len a1) + (len <*x1*>) by FINSEQ_1:22 .= (len a2) + 1 by A8, FINSEQ_1:40 .= (len a2) + (len <*(f . (i - (len p)))*>) by FINSEQ_1:40 .= len (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:22 ; A90: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def_3 .= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22 .= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22 .= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40 .= Seg (((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:40 .= Seg ((len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:22 .= Seg (len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1)) by FINSEQ_1:22 .= dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) by FINSEQ_1:def_3 ; consider n1 being Element of NAT such that A91: n1 in dom b1 and A92: k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 by A88; ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = b1 . n1 by A91, A92, FINSEQ_1:def_7 .= x . k by A13, A91, A92, A89, FINSEQ_1:def_7 ; hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A80, A90; ::_thesis: verum end; end; end; hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum end; A93: 1 <= j by A58, XREAL_1:19; j <= len f by A23, A26, A58, XREAL_1:19; then A94: i - (len p) in Seg (len f) by A93, FINSEQ_1:1; A95: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def_3 .= dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; A96: len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22 .= ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22 .= ((len a2) + 1) + (len b1) by FINSEQ_1:40 .= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40 .= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22 .= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22 .= len (the_arity_of o) by A95, FINSEQ_1:6 ; len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22 .= ((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22 .= ((len a2) + 1) + (len b1) by FINSEQ_1:40 .= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40 .= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22 .= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22 .= len (the_arity_of o) by A95, FINSEQ_1:6 ; then reconsider d1 = (a2 ^ <*(f . (i - (len p)))*>) ^ b1, d2 = (a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1 as Element of Args (o,A) by A79, A65, A96, MSAFREE2:5; A97: q . i = g . (i - (len p)) by A26, A58, FINSEQ_1:23 .= (Den (o,A)) . d1 by A23, A24, A94 ; (i + 1) - (len p) = (i - (len p)) + 1 by XCMPLX_1:29; then A98: [(f . (i - (len p))),(f . ((i + 1) - (len p)))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A62, A60; A99: i + 1 <= len q by A58, NAT_1:13; (len p) + 1 <= i + 1 by A58, NAT_1:12; then q . (i + 1) = g . ((i + 1) - (len p)) by A26, A99, FINSEQ_1:23 .= (Den (o,A)) . d2 by A23, A24, A61 ; hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A7, A8, A97, A98, Th12; ::_thesis: verum end; end; end; hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ; ::_thesis: verum end; end; hence [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) by A1, A4, A14, EQREL_1:28; ::_thesis: verum end; theorem Th14: :: MSUALG_5:14 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for o being OperSymbol of S for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for o being OperSymbol of S for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) set b1 = {} ; let o be OperSymbol of S; ::_thesis: for C1, C2 being MSCongruence of A for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) let C1, C2 be MSCongruence of A; ::_thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) let C be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( C = C1 "\/" C2 implies for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) ) assume A1: C = C1 "\/" C2 ; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) ) defpred S1[ Element of NAT ] means for a1, a2, b1 being FinSequence st len a1 = $1 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds [(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o); A2: for l being Element of NAT st S1[l] holds S1[l + 1] proof let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A3: for a1, a2, b1 being FinSequence st len a1 = l & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds [(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) ; ::_thesis: S1[l + 1] let a1, a2, b1 be FinSequence; ::_thesis: ( len a1 = l + 1 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds [(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) ) assume that A4: len a1 = l + 1 and A5: len a1 = len a2 and A6: x = a1 ^ b1 and A7: for n being Nat st n in dom a1 holds [(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) A8: l + 1 in Seg (len a1) by A4, FINSEQ_1:4; then A9: l + 1 in dom a2 by A5, FINSEQ_1:def_3; set y = a2 ^ b1; a2 <> {} by A4, A5; then consider q2 being FinSequence, y1 being set such that A10: a2 = q2 ^ <*y1*> by FINSEQ_1:46; A11: l + 1 = (len q2) + (len <*y1*>) by A4, A5, A10, FINSEQ_1:22 .= (len q2) + 1 by FINSEQ_1:40 ; then A12: y1 = a2 . (l + 1) by A10, FINSEQ_1:42 .= (a2 ^ b1) . (l + 1) by A9, FINSEQ_1:def_7 ; a1 <> {} by A4; then consider q1 being FinSequence, x1 being set such that A13: a1 = q1 ^ <*x1*> by FINSEQ_1:46; A14: l + 1 = (len q1) + (len <*x1*>) by A4, A13, FINSEQ_1:22 .= (len q1) + 1 by FINSEQ_1:40 ; then A15: len q1 = len q2 by A11, XCMPLX_1:2; A16: dom q1 = Seg (len q1) by FINSEQ_1:def_3 .= dom q2 by A15, FINSEQ_1:def_3 ; A17: for n being Element of NAT st n in dom q1 holds [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) proof let n be Element of NAT ; ::_thesis: ( n in dom q1 implies [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) ) len q1 <= len a1 by A4, A14, NAT_1:11; then A18: Seg (len q1) c= Seg (len a1) by FINSEQ_1:5; assume A19: n in dom q1 ; ::_thesis: [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) then n in Seg (len q1) by FINSEQ_1:def_3; then n in Seg (len a1) by A18; then A20: n in dom a1 by FINSEQ_1:def_3; then A21: x . n = a1 . n by A6, FINSEQ_1:def_7 .= q1 . n by A13, A19, FINSEQ_1:def_7 ; dom a1 = Seg (len a1) by FINSEQ_1:def_3 .= dom a2 by A5, FINSEQ_1:def_3 ; then (a2 ^ b1) . n = a2 . n by A20, FINSEQ_1:def_7 .= q2 . n by A10, A16, A19, FINSEQ_1:def_7 ; hence [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) by A7, A20, A21; ::_thesis: verum end; A22: l + 1 in dom a1 by A8, FINSEQ_1:def_3; A23: (q1 ^ <*x1*>) ^ b1 = q1 ^ (<*x1*> ^ b1) by FINSEQ_1:32; A24: (q2 ^ <*x1*>) ^ b1 = q2 ^ (<*x1*> ^ b1) by FINSEQ_1:32; A25: for n being Nat st n in dom q1 holds [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) proof let n be Nat; ::_thesis: ( n in dom q1 implies [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) ) assume A26: n in dom q1 ; ::_thesis: [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) then A27: ((q2 ^ <*x1*>) ^ b1) . n = q2 . n by A16, A24, FINSEQ_1:def_7; x . n = q1 . n by A6, A13, A23, A26, FINSEQ_1:def_7; hence [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) by A17, A26, A27; ::_thesis: verum end; x1 = a1 . (l + 1) by A13, A14, FINSEQ_1:42 .= x . (l + 1) by A6, A22, FINSEQ_1:def_7 ; then A28: [x1,y1] in C . ((the_arity_of o) /. (l + 1)) by A7, A22, A12; len q1 = l by A14, XCMPLX_1:2; then [((Den (o,A)) . x),((Den (o,A)) . ((q2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) by A3, A6, A13, A15, A23, A24, A25; hence [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) by A1, A6, A13, A10, A14, A15, A17, A28, Th13; ::_thesis: verum end; A29: dom y = dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; dom x = dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; then reconsider a1 = x, a2 = y as FinSequence by A29, FINSEQ_1:def_2; assume A30: for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) A31: Seg (len a2) = dom a2 by FINSEQ_1:def_3 .= dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; Seg (len a1) = dom a1 by FINSEQ_1:def_3 .= dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; then A32: len a1 = len a2 by A31, FINSEQ_1:6; A33: x = a1 ^ {} by FINSEQ_1:34; A34: y = a2 ^ {} by FINSEQ_1:34; A35: S1[ 0 ] proof field (C . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by ORDERS_1:12; then A36: C . (the_result_sort_of o) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def_9; A37: the Sorts of A . (the_result_sort_of o) = the Sorts of A . ( the ResultSort of S . o) by MSUALG_1:def_2 .= ( the Sorts of A * the ResultSort of S) . o by FUNCT_2:15 .= Result (o,A) by MSUALG_1:def_5 ; let a1, a2, b1 be FinSequence; ::_thesis: ( len a1 = 0 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds [(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) ) assume that A38: len a1 = 0 and A39: len a1 = len a2 and A40: x = a1 ^ b1 and for n being Nat st n in dom a1 holds [(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) A41: a1 = {} by A38; a2 = {} by A38, A39; hence [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) by A40, A41, A37, A36, RELAT_2:def_1; ::_thesis: verum end; for l being Element of NAT holds S1[l] from NAT_1:sch_1(A35, A2); hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by A30, A32, A33, A34; ::_thesis: verum end; theorem Th15: :: MSUALG_5:15 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A let C1, C2 be MSCongruence of A; ::_thesis: C1 "\/" C2 is MSCongruence of A reconsider C = C1 "\/" C2 as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ; reconsider C = C as ManySortedRelation of A ; reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; for o being OperSymbol of S for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by Th14; hence C1 "\/" C2 is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; theorem Th16: :: MSUALG_5:16 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A let C1, C2 be MSCongruence of A; ::_thesis: C1 /\ C2 is MSCongruence of A reconsider C = C1 /\ C2 as Equivalence_Relation of the Sorts of A by Th11; reconsider C = C as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ; reconsider C = C as ManySortedRelation of A ; reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; for o being OperSymbol of S for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) proof let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) ) assume A1: for n being Nat st n in dom x holds [(x . n),(y . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) for n being Nat st n in dom x holds [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) proof let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) ) assume n in dom x ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) then [(x . n),(y . n)] in C . ((the_arity_of o) /. n) by A1; then [(x . n),(y . n)] in (C1 . ((the_arity_of o) /. n)) /\ (C2 . ((the_arity_of o) /. n)) by PBOOLE:def_5; hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by XBOOLE_0:def_4; ::_thesis: verum end; then A2: [((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o) by MSUALG_4:def_4; for n being Nat st n in dom x holds [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) proof let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) ) assume n in dom x ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) then [(x . n),(y . n)] in C . ((the_arity_of o) /. n) by A1; then [(x . n),(y . n)] in (C1 . ((the_arity_of o) /. n)) /\ (C2 . ((the_arity_of o) /. n)) by PBOOLE:def_5; hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by XBOOLE_0:def_4; ::_thesis: verum end; then A3: [((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o) by MSUALG_4:def_4; (C1 . (the_result_sort_of o)) /\ (C2 . (the_result_sort_of o)) = C . (the_result_sort_of o) by PBOOLE:def_5; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by A2, A3, XBOOLE_0:def_4; ::_thesis: verum end; hence C1 /\ C2 is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means :Def6: :: MSUALG_5:def 6 for x being set holds ( x in the carrier of it iff x is MSCongruence of A ); existence ex b1 being strict SubLattice of EqRelLatt the Sorts of A st for x being set holds ( x in the carrier of b1 iff x is MSCongruence of A ) proof set D = the carrier of (EqRelLatt the Sorts of A); set f = the MSCongruence of A; defpred S1[ set ] means $1 is MSCongruence of A; deffunc H1( Element of S) -> set = bool [:( the Sorts of A . $1),( the Sorts of A . $1):]; consider M2 being ManySortedSet of the carrier of S such that A1: for i being Element of the carrier of S holds M2 . i = H1(i) from PBOOLE:sch_5(); consider B being set such that A2: for x being set holds ( x in B iff ( x in product M2 & S1[x] ) ) from XBOOLE_0:sch_1(); A3: for C1 being MSCongruence of A holds C1 in product M2 proof let C1 be MSCongruence of A; ::_thesis: C1 in product M2 A4: now__::_thesis:_for_x_being_set_st_x_in_dom_M2_holds_ C1_._x_in_M2_._x let x be set ; ::_thesis: ( x in dom M2 implies C1 . x in M2 . x ) assume x in dom M2 ; ::_thesis: C1 . x in M2 . x then reconsider x9 = x as Element of the carrier of S ; A5: C1 . x9 is Subset of [:( the Sorts of A . x9),( the Sorts of A . x9):] ; M2 . x9 = bool [:( the Sorts of A . x9),( the Sorts of A . x9):] by A1; hence C1 . x in M2 . x by A5; ::_thesis: verum end; dom C1 = the carrier of S by PARTFUN1:def_2 .= dom M2 by PARTFUN1:def_2 ; hence C1 in product M2 by A4, CARD_3:9; ::_thesis: verum end; A6: for x being set holds ( x in B iff x is MSCongruence of A ) proof let x be set ; ::_thesis: ( x in B iff x is MSCongruence of A ) thus ( x in B implies x is MSCongruence of A ) by A2; ::_thesis: ( x is MSCongruence of A implies x in B ) thus ( x is MSCongruence of A implies x in B ) ::_thesis: verum proof assume A7: x is MSCongruence of A ; ::_thesis: x in B then x in product M2 by A3; hence x in B by A2, A7; ::_thesis: verum end; end; then the MSCongruence of A in B ; then reconsider B = B as non empty set ; set B1 = the L_join of (EqRelLatt the Sorts of A) || B; set B2 = the L_meet of (EqRelLatt the Sorts of A) || B; now__::_thesis:_for_x_being_set_st_x_in_B_holds_ x_in_the_carrier_of_(EqRelLatt_the_Sorts_of_A) let x be set ; ::_thesis: ( x in B implies x in the carrier of (EqRelLatt the Sorts of A) ) assume x in B ; ::_thesis: x in the carrier of (EqRelLatt the Sorts of A) then x is MSCongruence of A by A6; hence x in the carrier of (EqRelLatt the Sorts of A) by Def5; ::_thesis: verum end; then A8: B c= the carrier of (EqRelLatt the Sorts of A) by TARSKI:def_3; then [:B,B:] c= [: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):] by ZFMISC_1:96; then reconsider B1 = the L_join of (EqRelLatt the Sorts of A) || B, B2 = the L_meet of (EqRelLatt the Sorts of A) || B as Function of [:B,B:], the carrier of (EqRelLatt the Sorts of A) by FUNCT_2:32; A9: dom B2 = [:B,B:] by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_[:B,B:]_holds_ B2_._x_in_B let x be set ; ::_thesis: ( x in [:B,B:] implies B2 . x in B ) assume A10: x in [:B,B:] ; ::_thesis: B2 . x in B then consider x1, x2 being set such that A11: x = [x1,x2] by RELAT_1:def_1; A12: x2 in B by A10, A11, ZFMISC_1:87; x1 in B by A10, A11, ZFMISC_1:87; then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A12; A13: x29 in B by A6; x19 in B by A6; then [x1,x2] in [:B,B:] by A13, ZFMISC_1:87; then B2 . x = the L_meet of (EqRelLatt the Sorts of A) . (x1,x2) by A11, FUNCT_1:49 .= x19 /\ x29 by Def5 ; then B2 . x is MSCongruence of A by Th16; hence B2 . x in B by A6; ::_thesis: verum end; then reconsider B2 = B2 as BinOp of B by A9, FUNCT_2:3; A14: dom B1 = [:B,B:] by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_[:B,B:]_holds_ B1_._x_in_B let x be set ; ::_thesis: ( x in [:B,B:] implies B1 . x in B ) assume A15: x in [:B,B:] ; ::_thesis: B1 . x in B then consider x1, x2 being set such that A16: x = [x1,x2] by RELAT_1:def_1; A17: x2 in B by A15, A16, ZFMISC_1:87; x1 in B by A15, A16, ZFMISC_1:87; then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A17; A18: x29 in B by A6; x19 in B by A6; then [x1,x2] in [:B,B:] by A18, ZFMISC_1:87; then B1 . x = the L_join of (EqRelLatt the Sorts of A) . (x1,x2) by A16, FUNCT_1:49 .= x19 "\/" x29 by Def5 ; then B1 . x is MSCongruence of A by Th15; hence B1 . x in B by A6; ::_thesis: verum end; then reconsider B1 = B1 as BinOp of B by A14, FUNCT_2:3; reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ; A19: for a, b being MSCongruence of A holds ( B1 . (a,b) = a "\/" b & B2 . (a,b) = a /\ b ) proof let a, b be MSCongruence of A; ::_thesis: ( B1 . (a,b) = a "\/" b & B2 . (a,b) = a /\ b ) A20: b in B by A6; a in B by A6; then A21: [a,b] in [:B,B:] by A20, ZFMISC_1:87; hence B1 . (a,b) = the L_join of (EqRelLatt the Sorts of A) . (a,b) by FUNCT_1:49 .= a "\/" b by Def5 ; ::_thesis: B2 . (a,b) = a /\ b thus B2 . (a,b) = the L_meet of (EqRelLatt the Sorts of A) . (a,b) by A21, FUNCT_1:49 .= a /\ b by Def5 ; ::_thesis: verum end; A22: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B1_._(a,b)_=_B1_._(b,a) let a, b be Element of B; ::_thesis: B1 . (a,b) = B1 . (b,a) reconsider a9 = a, b9 = b as MSCongruence of A by A6; thus B1 . (a,b) = a9 "\/" b9 by A19 .= B1 . (b,a) by A19 ; ::_thesis: verum end; A23: for a, b being Element of L holds a "\/" b = b "\/" a proof let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a thus a "\/" b = B1 . (a,b) by LATTICES:def_1 .= the L_join of L . (b,a) by A22 .= b "\/" a by LATTICES:def_1 ; ::_thesis: verum end; A24: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B2_._(a,(B2_._(b,c)))_=_B2_._((B2_._(a,b)),c) let a, b, c be Element of B; ::_thesis: B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c) reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6; reconsider e1 = b9 /\ c9 as MSCongruence of A by Th16; reconsider e2 = a9 /\ b9 as MSCongruence of A by Th16; thus B2 . (a,(B2 . (b,c))) = B2 . (a,e1) by A19 .= a9 /\ (b9 /\ c9) by A19 .= (a9 /\ b9) /\ c9 by PBOOLE:29 .= B2 . (e2,c) by A19 .= B2 . ((B2 . (a,b)),c) by A19 ; ::_thesis: verum end; A25: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def_2 .= B2 . (a,(B2 . (b,c))) by LATTICES:def_2 .= the L_meet of L . (( the L_meet of L . (a,b)),c) by A24 .= the L_meet of L . ((a "/\" b),c) by LATTICES:def_2 .= (a "/\" b) "/\" c by LATTICES:def_2 ; ::_thesis: verum end; A26: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B1_._(a,(B1_._(b,c)))_=_B1_._((B1_._(a,b)),c) let a, b, c be Element of B; ::_thesis: B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c) reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6; reconsider d = b9 "\/" c9 as MSCongruence of A by Th15; reconsider e = a9 "\/" b9 as MSCongruence of A by Th15; thus B1 . (a,(B1 . (b,c))) = B1 . (a,d) by A19 .= a9 "\/" (b9 "\/" c9) by A19 .= (a9 "\/" b9) "\/" c9 by Th8 .= B1 . (e,c) by A19 .= B1 . ((B1 . (a,b)),c) by A19 ; ::_thesis: verum end; A27: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def_1 .= B1 . (a,(B1 . (b,c))) by LATTICES:def_1 .= the L_join of L . (( the L_join of L . (a,b)),c) by A26 .= the L_join of L . ((a "\/" b),c) by LATTICES:def_1 .= (a "\/" b) "\/" c by LATTICES:def_1 ; ::_thesis: verum end; A28: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B2_._(a,b)_=_B2_._(b,a) let a, b be Element of B; ::_thesis: B2 . (a,b) = B2 . (b,a) reconsider a9 = a, b9 = b as MSCongruence of A by A6; thus B2 . (a,b) = b9 /\ a9 by A19 .= B2 . (b,a) by A19 ; ::_thesis: verum end; A29: for a, b being Element of L holds a "/\" b = b "/\" a proof let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a thus a "/\" b = B2 . (a,b) by LATTICES:def_2 .= the L_meet of L . (b,a) by A28 .= b "/\" a by LATTICES:def_2 ; ::_thesis: verum end; A30: for a, b being Element of L holds a "/\" (a "\/" b) = a proof let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a A31: B2 . (a,(B1 . (a,b))) = a proof reconsider a9 = a, b9 = b as MSCongruence of A by A6; reconsider d = a9 "\/" b9 as MSCongruence of A by Th15; thus B2 . (a,(B1 . (a,b))) = B2 . (a,d) by A19 .= a9 /\ (a9 "\/" b9) by A19 .= a by Th9 ; ::_thesis: verum end; thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def_2 .= a by A31, LATTICES:def_1 ; ::_thesis: verum end; for a, b being Element of L holds (a "/\" b) "\/" b = b proof let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b A32: B1 . ((B2 . (a,b)),b) = b proof reconsider a9 = a, b9 = b as MSCongruence of A by A6; reconsider EQR = a9 /\ b9 as MSCongruence of A by Th16; thus B1 . ((B2 . (a,b)),b) = B1 . ((a9 /\ b9),b9) by A19 .= EQR "\/" b9 by A19 .= b by Th10 ; ::_thesis: verum end; thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def_1 .= b by A32, LATTICES:def_2 ; ::_thesis: verum end; then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A23, A27, A29, A25, A30, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; then reconsider L = L as Lattice ; reconsider L = L as strict SubLattice of EqRelLatt the Sorts of A by A8, NAT_LAT:def_12; take L ; ::_thesis: for x being set holds ( x in the carrier of L iff x is MSCongruence of A ) thus for x being set holds ( x in the carrier of L iff x is MSCongruence of A ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being strict SubLattice of EqRelLatt the Sorts of A st ( for x being set holds ( x in the carrier of b1 iff x is MSCongruence of A ) ) & ( for x being set holds ( x in the carrier of b2 iff x is MSCongruence of A ) ) holds b1 = b2 proof let C1, C2 be strict SubLattice of EqRelLatt the Sorts of A; ::_thesis: ( ( for x being set holds ( x in the carrier of C1 iff x is MSCongruence of A ) ) & ( for x being set holds ( x in the carrier of C2 iff x is MSCongruence of A ) ) implies C1 = C2 ) assume that A33: for x being set holds ( x in the carrier of C1 iff x is MSCongruence of A ) and A34: for x being set holds ( x in the carrier of C2 iff x is MSCongruence of A ) ; ::_thesis: C1 = C2 A35: now__::_thesis:_for_x_being_set_holds_ (_x_in_the_carrier_of_C1_iff_x_in_the_carrier_of_C2_) let x be set ; ::_thesis: ( x in the carrier of C1 iff x in the carrier of C2 ) ( x in the carrier of C2 iff x is MSCongruence of A ) by A34; hence ( x in the carrier of C1 iff x in the carrier of C2 ) by A33; ::_thesis: verum end; then A36: the carrier of C1 = the carrier of C2 by TARSKI:1; then A37: the L_join of C1 = the L_join of (EqRelLatt the Sorts of A) || the carrier of C2 by NAT_LAT:def_12 .= the L_join of C2 by NAT_LAT:def_12 ; the L_meet of C1 = the L_meet of (EqRelLatt the Sorts of A) || the carrier of C2 by A36, NAT_LAT:def_12 .= the L_meet of C2 by NAT_LAT:def_12 ; hence C1 = C2 by A35, A37, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def6 defines CongrLatt MSUALG_5:def_6_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for b3 being strict SubLattice of EqRelLatt the Sorts of A holds ( b3 = CongrLatt A iff for x being set holds ( x in the carrier of b3 iff x is MSCongruence of A ) ); theorem Th17: :: MSUALG_5:17 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: id the Sorts of A is MSCongruence of A set J = id the Sorts of A; for i being set st i in the carrier of S holds (id the Sorts of A) . i is Relation of ( the Sorts of A . i) proof let i be set ; ::_thesis: ( i in the carrier of S implies (id the Sorts of A) . i is Relation of ( the Sorts of A . i) ) assume i in the carrier of S ; ::_thesis: (id the Sorts of A) . i is Relation of ( the Sorts of A . i) then (id the Sorts of A) . i = id ( the Sorts of A . i) by MSUALG_3:def_1; hence (id the Sorts of A) . i is Relation of ( the Sorts of A . i) ; ::_thesis: verum end; then reconsider J = id the Sorts of A as ManySortedRelation of the Sorts of A by MSUALG_4:def_1; for i being set for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds R is Equivalence_Relation of ( the Sorts of A . i) proof let i be set ; ::_thesis: for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds R is Equivalence_Relation of ( the Sorts of A . i) let R be Relation of ( the Sorts of A . i); ::_thesis: ( i in the carrier of S & J . i = R implies R is Equivalence_Relation of ( the Sorts of A . i) ) assume that A1: i in the carrier of S and A2: J . i = R ; ::_thesis: R is Equivalence_Relation of ( the Sorts of A . i) J . i = id ( the Sorts of A . i) by A1, MSUALG_3:def_1; hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; ::_thesis: verum end; then reconsider J = J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def_2; reconsider J = J as ManySortedRelation of A ; reconsider J = J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; for o being OperSymbol of S for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) proof let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) ) assume A3: for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) A4: dom y = dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; A5: dom x = dom (the_arity_of o) by MSUALG_3:6 .= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ; then reconsider x9 = x, y9 = y as FinSequence by A4, FINSEQ_1:def_2; now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_ x9_._n_=_y9_._n let n be Nat; ::_thesis: ( n in dom x implies x9 . n = y9 . n ) assume A6: n in dom x ; ::_thesis: x9 . n = y9 . n J . ((the_arity_of o) /. n) = id ( the Sorts of A . ((the_arity_of o) /. n)) by MSUALG_3:def_1; then [(x . n),(y . n)] in id ( the Sorts of A . ((the_arity_of o) /. n)) by A3, A6; hence x9 . n = y9 . n by RELAT_1:def_10; ::_thesis: verum end; then A7: x = y by A5, A4, FINSEQ_1:13; (Den (o,A)) . x in Result (o,A) ; then A8: (Den (o,A)) . x in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5; o in the carrier' of S ; then o in dom the ResultSort of S by FUNCT_2:def_1; then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by A8, FUNCT_1:13; then A9: (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2; J . (the_result_sort_of o) = id ( the Sorts of A . (the_result_sort_of o)) by MSUALG_3:def_1; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) by A7, A9, RELAT_1:def_10; ::_thesis: verum end; hence id the Sorts of A is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; theorem Th18: :: MSUALG_5:18 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: [| the Sorts of A, the Sorts of A|] is MSCongruence of A set J = [| the Sorts of A, the Sorts of A|]; for i being set st i in the carrier of S holds [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) proof let i be set ; ::_thesis: ( i in the carrier of S implies [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) ) assume i in the carrier of S ; ::_thesis: [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) then [| the Sorts of A, the Sorts of A|] . i c= [:( the Sorts of A . i),( the Sorts of A . i):] by PBOOLE:def_16; hence [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) ; ::_thesis: verum end; then reconsider J = [| the Sorts of A, the Sorts of A|] as ManySortedRelation of the Sorts of A by MSUALG_4:def_1; for i being set for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds R is Equivalence_Relation of ( the Sorts of A . i) proof let i be set ; ::_thesis: for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds R is Equivalence_Relation of ( the Sorts of A . i) let R be Relation of ( the Sorts of A . i); ::_thesis: ( i in the carrier of S & J . i = R implies R is Equivalence_Relation of ( the Sorts of A . i) ) assume that A1: i in the carrier of S and A2: J . i = R ; ::_thesis: R is Equivalence_Relation of ( the Sorts of A . i) J . i = nabla ( the Sorts of A . i) by A1, PBOOLE:def_16; hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; ::_thesis: verum end; then reconsider J = J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def_2; reconsider J = J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; for o being OperSymbol of S for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) proof let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) ) assume for n being Nat st n in dom x holds [(x . n),(y . n)] in J . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) o in the carrier' of S ; then A3: o in dom the ResultSort of S by FUNCT_2:def_1; (Den (o,A)) . y in Result (o,A) ; then (Den (o,A)) . y in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5; then (Den (o,A)) . y in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13; then A4: (Den (o,A)) . y in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2; (Den (o,A)) . x in Result (o,A) ; then (Den (o,A)) . x in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5; then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13; then A5: (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2; J . (the_result_sort_of o) = [:( the Sorts of A . (the_result_sort_of o)),( the Sorts of A . (the_result_sort_of o)):] by PBOOLE:def_16; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) by A5, A4, ZFMISC_1:87; ::_thesis: verum end; hence [| the Sorts of A, the Sorts of A|] is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; cluster CongrLatt A -> strict bounded ; coherence CongrLatt A is bounded proof ex c being Element of (CongrLatt A) st for a being Element of (CongrLatt A) holds ( c "\/" a = c & a "\/" c = c ) proof reconsider c9 = [| the Sorts of A, the Sorts of A|] as MSCongruence of A by Th18; A1: the L_join of (CongrLatt A) = the L_join of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12; reconsider c = c9 as Element of (CongrLatt A) by Def6; take c ; ::_thesis: for a being Element of (CongrLatt A) holds ( c "\/" a = c & a "\/" c = c ) let a be Element of (CongrLatt A); ::_thesis: ( c "\/" a = c & a "\/" c = c ) A2: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87; reconsider a9 = a as MSCongruence of A by Def6; A3: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (c9_"\/"_a9)_._i_=_c9_._i let i be set ; ::_thesis: ( i in the carrier of S implies (c9 "\/" a9) . i = c9 . i ) assume A4: i in the carrier of S ; ::_thesis: (c9 "\/" a9) . i = c9 . i then reconsider i9 = i as Element of S ; A5: ex K1 being ManySortedRelation of the Sorts of A st ( K1 = c9 \/ a9 & c9 "\/" a9 = EqCl K1 ) by Def4; reconsider K2 = c9 . i9, a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) ; (c9 \/ a9) . i = (c9 . i) \/ (a9 . i) by A4, PBOOLE:def_4 .= (nabla ( the Sorts of A . i)) \/ a2 by PBOOLE:def_16 .= nabla ( the Sorts of A . i) by EQREL_1:1 .= c9 . i by A4, PBOOLE:def_16 ; hence (c9 "\/" a9) . i = EqCl K2 by A5, Def3 .= c9 . i by Th2 ; ::_thesis: verum end; thus c "\/" a = the L_join of (CongrLatt A) . (c,a) by LATTICES:def_1 .= the L_join of (EqRelLatt the Sorts of A) . (c,a) by A1, A2, FUNCT_1:49 .= c9 "\/" a9 by Def5 .= c by A3, PBOOLE:3 ; ::_thesis: a "\/" c = c hence a "\/" c = c ; ::_thesis: verum end; then A6: CongrLatt A is upper-bounded by LATTICES:def_14; ex c being Element of (CongrLatt A) st for a being Element of (CongrLatt A) holds ( c "/\" a = c & a "/\" c = c ) proof reconsider c9 = id the Sorts of A as MSCongruence of A by Th17; A7: the L_meet of (CongrLatt A) = the L_meet of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12; reconsider c = c9 as Element of (CongrLatt A) by Def6; take c ; ::_thesis: for a being Element of (CongrLatt A) holds ( c "/\" a = c & a "/\" c = c ) let a be Element of (CongrLatt A); ::_thesis: ( c "/\" a = c & a "/\" c = c ) A8: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87; reconsider a9 = a as MSCongruence of A by Def6; A9: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (c9_/\_a9)_._i_=_c9_._i let i be set ; ::_thesis: ( i in the carrier of S implies (c9 /\ a9) . i = c9 . i ) assume A10: i in the carrier of S ; ::_thesis: (c9 /\ a9) . i = c9 . i then reconsider i9 = i as Element of S ; reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) ; thus (c9 /\ a9) . i = (c9 . i) /\ (a9 . i) by A10, PBOOLE:def_5 .= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def_1 .= id ( the Sorts of A . i) by EQREL_1:10 .= c9 . i by A10, MSUALG_3:def_1 ; ::_thesis: verum end; thus c "/\" a = the L_meet of (CongrLatt A) . (c,a) by LATTICES:def_2 .= the L_meet of (EqRelLatt the Sorts of A) . (c,a) by A7, A8, FUNCT_1:49 .= c9 /\ a9 by Def5 .= c by A9, PBOOLE:3 ; ::_thesis: a "/\" c = c hence a "/\" c = c ; ::_thesis: verum end; then CongrLatt A is lower-bounded by LATTICES:def_13; hence CongrLatt A is bounded by A6; ::_thesis: verum end; end; theorem :: MSUALG_5:19 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A let A be non-empty MSAlgebra over S; ::_thesis: Bottom (CongrLatt A) = id the Sorts of A set K = id the Sorts of A; id the Sorts of A is MSCongruence of A by Th17; then reconsider K = id the Sorts of A as Element of (CongrLatt A) by Def6; A1: the L_meet of (CongrLatt A) = the L_meet of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12; now__::_thesis:_for_a_being_Element_of_(CongrLatt_A)_holds_ (_K_"/\"_a_=_K_&_a_"/\"_K_=_K_) let a be Element of (CongrLatt A); ::_thesis: ( K "/\" a = K & a "/\" K = K ) reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6; A2: [K,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87; A3: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (K9_/\_a9)_._i_=_K9_._i let i be set ; ::_thesis: ( i in the carrier of S implies (K9 /\ a9) . i = K9 . i ) assume A4: i in the carrier of S ; ::_thesis: (K9 /\ a9) . i = K9 . i then reconsider i9 = i as Element of S ; reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def_2; thus (K9 /\ a9) . i = (K9 . i) /\ (a9 . i) by A4, PBOOLE:def_5 .= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def_1 .= id ( the Sorts of A . i) by EQREL_1:10 .= K9 . i by A4, MSUALG_3:def_1 ; ::_thesis: verum end; thus K "/\" a = the L_meet of (CongrLatt A) . (K,a) by LATTICES:def_2 .= the L_meet of (EqRelLatt the Sorts of A) . (K,a) by A1, A2, FUNCT_1:49 .= K9 /\ a9 by Def5 .= K by A3, PBOOLE:3 ; ::_thesis: a "/\" K = K hence a "/\" K = K ; ::_thesis: verum end; hence Bottom (CongrLatt A) = id the Sorts of A by LATTICES:def_16; ::_thesis: verum end; theorem :: MSUALG_5:20 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|] proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|] let A be non-empty MSAlgebra over S; ::_thesis: Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|] set K = [| the Sorts of A, the Sorts of A|]; [| the Sorts of A, the Sorts of A|] is MSCongruence of A by Th18; then reconsider K = [| the Sorts of A, the Sorts of A|] as Element of (CongrLatt A) by Def6; A1: the L_join of (CongrLatt A) = the L_join of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12; now__::_thesis:_for_a_being_Element_of_(CongrLatt_A)_holds_ (_K_"\/"_a_=_K_&_a_"\/"_K_=_K_) let a be Element of (CongrLatt A); ::_thesis: ( K "\/" a = K & a "\/" K = K ) reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6; A2: [K,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87; A3: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (K9_"\/"_a9)_._i_=_K9_._i let i be set ; ::_thesis: ( i in the carrier of S implies (K9 "\/" a9) . i = K9 . i ) assume A4: i in the carrier of S ; ::_thesis: (K9 "\/" a9) . i = K9 . i then reconsider i9 = i as Element of S ; A5: ex K1 being ManySortedRelation of the Sorts of A st ( K1 = K9 \/ a9 & K9 "\/" a9 = EqCl K1 ) by Def4; reconsider K2 = K9 . i9, a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def_2; (K9 \/ a9) . i = (K9 . i) \/ (a9 . i) by A4, PBOOLE:def_4 .= (nabla ( the Sorts of A . i)) \/ a2 by PBOOLE:def_16 .= nabla ( the Sorts of A . i) by EQREL_1:1 .= K9 . i by A4, PBOOLE:def_16 ; hence (K9 "\/" a9) . i = EqCl K2 by A5, Def3 .= K9 . i by Th2 ; ::_thesis: verum end; thus K "\/" a = the L_join of (CongrLatt A) . (K,a) by LATTICES:def_1 .= the L_join of (EqRelLatt the Sorts of A) . (K,a) by A1, A2, FUNCT_1:49 .= K9 "\/" a9 by Def5 .= K by A3, PBOOLE:3 ; ::_thesis: a "\/" K = K hence a "\/" K = K ; ::_thesis: verum end; hence Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|] by LATTICES:def_17; ::_thesis: verum end; theorem :: MSUALG_5:21 for x, X being set holds ( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X ) proof let x, X be set ; ::_thesis: ( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X ) A1: the carrier of (EqRelLatt X) = { x1 where x1 is Relation of X,X : x1 is Equivalence_Relation of X } by Def2; thus ( x in the carrier of (EqRelLatt X) implies x is Equivalence_Relation of X ) ::_thesis: ( x is Equivalence_Relation of X implies x in the carrier of (EqRelLatt X) ) proof assume x in the carrier of (EqRelLatt X) ; ::_thesis: x is Equivalence_Relation of X then ex x1 being Relation of X,X st ( x = x1 & x1 is Equivalence_Relation of X ) by A1; hence x is Equivalence_Relation of X ; ::_thesis: verum end; thus ( x is Equivalence_Relation of X implies x in the carrier of (EqRelLatt X) ) by A1; ::_thesis: verum end;