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;

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

hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
; :: thesis: verumper 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;

end;

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)

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;[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)

proof

then
[((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o)
by MSUALG_4:def 4;
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;

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

hence
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
; :: thesis: verumper 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;

end;

( 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;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

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)

( 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;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

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)

( 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;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

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

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)

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;[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)

proof

then
[((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o)
by MSUALG_4:def 4;
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;

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

hence
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
; :: thesis: verumper 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;

end;

( 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;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

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)

( 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;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

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)

( 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;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

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