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 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . )

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 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . )

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 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . )

let C1, C2 be MSCongruence of A; :: thesis: for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . )

let x1, y1 be set ; :: thesis: for a1, b1 being FinSequence st [x1,y1] in (C1 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . )

let a1, b1 be FinSequence; :: thesis: ( [x1,y1] in (C1 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . ) )

assume A1: [x1,y1] in (C1 . (() /. ((len a1) + 1))) \/ (C2 . (() /. ((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 . ) \/ (C2 . )

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 . ) \/ (C2 . ) )
assume that
A2: x = (a1 ^ <*x1*>) ^ b1 and
A3: y = (a1 ^ <*y1*>) ^ b1 ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . )
A4: y = a1 ^ (<*y1*> ^ b1) by ;
A5: x = a1 ^ (<*x1*> ^ b1) by ;
now :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . )
per cases ( [x1,y1] in C1 . (() /. ((len a1) + 1)) or [x1,y1] in C2 . (() /. ((len a1) + 1)) ) by ;
suppose A6: [x1,y1] in C1 . (() /. ((len a1) + 1)) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . )
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C1 . (() /. n)
proof
let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . (() /. n) )
assume A7: n in dom x ; :: thesis: [(x . n),(y . n)] in C1 . (() /. n)
then reconsider dz = dom () as non empty set by MSUALG_3:6;
A8: n in dom () by ;
then A9: n in dom ( the Sorts of A * ()) by PARTFUN1:def 2;
reconsider so = the Sorts of A * () 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 #) . ()),n) by MSUALG_1:def 1
.= pi ((product ( the Sorts of A * ())),n) by FINSEQ_2:def 5
.= ( the Sorts of A * ()) . n by
.= the Sorts of A . (() . n) by
.= the Sorts of A . (() /. n) by ;
then A11: x . n in the Sorts of A . (() /. 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 ;
now :: thesis: [(x . n),(y . n)] in C1 . (() /. n)
per cases ( 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 ;
suppose A13: n in dom a1 ; :: thesis: [(x . n),(y . n)] in C1 . (() /. n)
then A14: y . n = a1 . n by ;
x . n = a1 . n by ;
hence [(x . n),(y . n)] in C1 . (() /. n) by ; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) ; :: thesis: [(x . n),(y . n)] in C1 . (() /. 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 ;
then A18: m = 1 by ;
then A19: n in Seg ((len a1) + 1) by ;
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
.= y1 by FINSEQ_1:42 ;
n in Seg ((len a1) + (len <*x1*>)) by ;
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
.= x1 by FINSEQ_1:42 ;
hence [(x . n),(y . n)] in C1 . (() /. n) by ; :: 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 . (() /. 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 ;
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 ;
x . n = b1 . k by ;
hence [(x . n),(y . n)] in C1 . (() /. n) by ; :: thesis: verum
end;
end;
end;
hence [(x . n),(y . n)] in C1 . (() /. n) ; :: thesis: verum
end;
then [((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . by MSUALG_4:def 4;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . ) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A24: [x1,y1] in C2 . (() /. ((len a1) + 1)) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . )
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C2 . (() /. n)
proof
let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . (() /. n) )
assume A25: n in dom x ; :: thesis: [(x . n),(y . n)] in C2 . (() /. n)
then reconsider dz = dom () as non empty set by MSUALG_3:6;
A26: n in dom () by ;
then A27: n in dom ( the Sorts of A * ()) by PARTFUN1:def 2;
reconsider so = the Sorts of A * () 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 #) . ()),n) by MSUALG_1:def 1
.= pi ((product ( the Sorts of A * ())),n) by FINSEQ_2:def 5
.= ( the Sorts of A * ()) . n by
.= the Sorts of A . (() . n) by
.= the Sorts of A . (() /. n) by ;
then A29: x . n in the Sorts of A . (() /. 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 ;
now :: thesis: [(x . n),(y . n)] in C2 . (() /. n)
per cases ( 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 ;
suppose A31: n in dom a1 ; :: thesis: [(x . n),(y . n)] in C2 . (() /. n)
then A32: y . n = a1 . n by ;
x . n = a1 . n by ;
hence [(x . n),(y . n)] in C2 . (() /. n) by ; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) ; :: thesis: [(x . n),(y . n)] in C2 . (() /. 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 ;
then A36: m = 1 by ;
then A37: n in Seg ((len a1) + 1) by ;
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
.= y1 by FINSEQ_1:42 ;
n in Seg ((len a1) + (len <*x1*>)) by ;
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
.= x1 by FINSEQ_1:42 ;
hence [(x . n),(y . n)] in C2 . (() /. n) by ; :: 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 . (() /. 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 ;
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 ;
x . n = b1 . k by ;
hence [(x . n),(y . n)] in C2 . (() /. n) by ; :: thesis: verum
end;
end;
end;
hence [(x . n),(y . n)] in C2 . (() /. n) ; :: thesis: verum
end;
then [((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . by MSUALG_4:def 4;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . ) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . ) \/ (C2 . ) ; :: thesis: verum