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 S_{1}[ 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 Nat st S_{1}[l] holds

S_{1}[l + 1]

.= 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: S_{1}[ 0 ]
_{1}[l]
from NAT_1:sch 2(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

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 S

[(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 Nat st S

S

proof

A29: dom y =
dom (the_arity_of o)
by MSUALG_3:6
let l be Nat; :: thesis: ( S_{1}[l] implies S_{1}[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: S_{1}[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 object 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 object 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)

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)

.= 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;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: S

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 object 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 object 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

A22:
l + 1 in dom a1
by A8, FINSEQ_1:def 3;
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;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

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

x1 =
a1 . (l + 1)
by A13, A14, FINSEQ_1:42
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;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

.= 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

.= 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: S

proof

for l being Nat holds S
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;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

hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by A30, A32, A33, A34; :: thesis: verum