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

per cases ( [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;

suppose A6: [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 non-empty 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)

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 A12, FINSEQ_1:25;

suppose A13: 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;

suppose A24: [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 non-empty 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)

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 A30, FINSEQ_1:25;

suppose A31: 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