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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C .

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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C .

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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C .

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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C .

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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . )

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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C .

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 . (() /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in C . )

defpred S1[ 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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . ;
A2: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be 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 . (() /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . ; :: 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 . (() /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . )

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 . (() /. n) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C .
A8: l + 1 in Seg (len a1) by ;
then A9: l + 1 in dom a2 by ;
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
.= (len q2) + 1 by FINSEQ_1:40 ;
then A12: y1 = a2 . (l + 1) by
.= (a2 ^ b1) . (l + 1) by ;
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
.= (len q1) + 1 by FINSEQ_1:40 ;
then A15: len q1 = len q2 by ;
A16: dom q1 = Seg (len q1) by FINSEQ_1:def 3
.= dom q2 by ;
A17: for n being Element of NAT st n in dom q1 holds
[(q1 . n),(q2 . n)] in C . (() /. n)
proof
let n be Element of NAT ; :: thesis: ( n in dom q1 implies [(q1 . n),(q2 . n)] in C . (() /. n) )
len q1 <= len a1 by ;
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 . (() /. 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
.= q1 . n by ;
dom a1 = Seg (len a1) by FINSEQ_1:def 3
.= dom a2 by ;
then (a2 ^ b1) . n = a2 . n by
.= q2 . n by ;
hence [(q1 . n),(q2 . n)] in C . (() /. n) by A7, A20, A21; :: thesis: verum
end;
A22: l + 1 in dom a1 by ;
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 . (() /. n)
proof
let n be Nat; :: thesis: ( n in dom q1 implies [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . (() /. n) )
assume A26: n in dom q1 ; :: thesis: [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . (() /. n)
then A27: ((q2 ^ <*x1*>) ^ b1) . n = q2 . n by ;
x . n = q1 . n by ;
hence [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . (() /. n) by ; :: thesis: verum
end;
x1 = a1 . (l + 1) by
.= x . (l + 1) by ;
then A28: [x1,y1] in C . (() /. (l + 1)) by A7, A22, A12;
len q1 = l by ;
then [((Den (o,A)) . x),((Den (o,A)) . ((q2 ^ <*x1*>) ^ b1))] in C . by A3, A6, A13, A15, A23, A24, A25;
hence [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . by A1, A6, A13, A10, A14, A15, A17, A28, Th13; :: thesis: verum
end;
A29: dom y = dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
dom x = dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
then reconsider a1 = x, a2 = y as FinSequence by ;
assume A30: for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . (() /. n) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in C .
A31: Seg (len a2) = dom a2 by FINSEQ_1:def 3
.= dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
Seg (len a1) = dom a1 by FINSEQ_1:def 3
.= dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
then A32: len a1 = len a2 by ;
A33: x = a1 ^ {} by FINSEQ_1:34;
A34: y = a2 ^ {} by FINSEQ_1:34;
A35: S1[ 0 ]
proof
field (C . ) = the Sorts of A . by ORDERS_1:12;
then A36: C . is_reflexive_in the Sorts of A . by RELAT_2:def 9;
A37: the Sorts of A . = 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 . (() /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . )

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 . (() /. n) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C .
A41: a1 = {} by A38;
a2 = {} by ;
hence [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . by ; :: thesis: verum
end;
for l being Nat holds S1[l] from NAT_1:sch 2(A35, A2);
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . by A30, A32, A33, A34; :: thesis: verum