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 x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] 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 x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
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 x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] 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 x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let C be MSEquivalence-like ManySortedRelation of A; :: thesis: ( C = C1 "\/" C2 implies for x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
assume A1: C = C1 "\/" C2 ; :: thesis: for x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
consider C9 being ManySortedRelation of the Sorts of A such that
A2: C9 = C1 (\/) C2 and
A3: C1 "\/" C2 = EqCl C9 by Def4;
A4: (C1 . (the_result_sort_of o)) "\/" (C2 . (the_result_sort_of o)) = EqCl ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) by Th1
.= EqCl (C9 . (the_result_sort_of o)) by A2, PBOOLE:def 4
.= (C1 "\/" C2) . (the_result_sort_of o) by A3, Def3 ;
consider D9 being ManySortedRelation of the Sorts of A such that
A5: D9 = C1 (\/) C2 and
A6: C1 "\/" C2 = EqCl D9 by Def4;
let x1, y1 be object ; :: thesis: for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let n be Element of NAT ; :: thesis: for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let a1, a2, b1 be FinSequence; :: thesis: ( len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) implies for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
assume that
A7: len a1 = n and
A8: len a1 = len a2 and
A9: for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ; :: thesis: ( not [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) or not [x1,y1] in C . ((the_arity_of o) /. (n + 1)) or for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
A10: (C1 . ((the_arity_of o) /. (n + 1))) "\/" (C2 . ((the_arity_of o) /. (n + 1))) = EqCl ((C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1)))) by Th1
.= EqCl (D9 . ((the_arity_of o) /. (n + 1))) by A5, PBOOLE:def 4
.= (C1 "\/" C2) . ((the_arity_of o) /. (n + 1)) by A6, Def3 ;
set y = (a2 ^ <*y1*>) ^ b1;
assume that
A11: [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) and
A12: [x1,y1] in C . ((the_arity_of o) /. (n + 1)) ; :: thesis: for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let x be Element of Args (o,A); :: thesis: ( x = (a1 ^ <*x1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
assume A13: x = (a1 ^ <*x1*>) ^ b1 ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
A14: 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 ;
then (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ;
then consider p being FinSequence such that
A15: 1 <= len p and
A16: (Den (o,A)) . ((a1 ^ <*x1*>) ^ b1) = p . 1 and
A17: (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) = p . (len p) and
A18: for i being Nat st 1 <= i & i < len p holds
[(p . i),(p . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A1, A11, A13, A4, EQREL_1:28;
x1 in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A12, ZFMISC_1:87;
then consider f being FinSequence such that
A19: 1 <= len f and
A20: x1 = f . 1 and
A21: y1 = f . (len f) and
A22: for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A1, A12, A10, EQREL_1:28;
deffunc H₁( Nat) -> set = (Den (o,A)) . ((a2 ^ <*(f . $1)*>) ^ b1);
consider g being FinSequence such that
A23: ( len g = len f & ( for i being Nat st i in dom g holds
g . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A24: dom g = Seg (len f) by A23, FINSEQ_1:def 3;
A25: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3
.= Seg (len (a1 ^ (<*x1*> ^ b1))) by FINSEQ_1:32
.= Seg ((len a2) + (len (<*x1*> ^ b1))) by A8, FINSEQ_1:22
.= Seg (len (a2 ^ (<*x1*> ^ b1))) by FINSEQ_1:22
.= Seg (len ((a2 ^ <*x1*>) ^ b1)) by FINSEQ_1:32
.= dom ((a2 ^ <*x1*>) ^ b1) by FINSEQ_1:def 3 ;
ex q being FinSequence st
( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

proof

take q = p ^ g; :: thesis: ( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
A26: len q = (len p) + (len g) by FINSEQ_1:22;
hence 1 <= len q by A15, NAT_1:12; :: thesis: ( (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
1 in dom p by A15, FINSEQ_3:25;
hence q . 1 = (Den (o,A)) . x by A13, A16, FINSEQ_1:def 7; :: thesis: ( (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
A27: len g in Seg (len f) by A19, A23, FINSEQ_1:1;
then len g in dom g by A23, FINSEQ_1:def 3;
hence q . (len q) = g . (len g) by A26, FINSEQ_1:def 7
.= (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) by A21, A23, A24, A27 ;
:: thesis: for i being Nat st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
A28: len p <> 0 by A15;

hereby :: thesis: verum

let i be Nat; :: thesis: ( 1 <= i & i < len q implies [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )
assume that
A29: 1 <= i and
A30: i < len q ; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
A31: ( ( 1 <= i & i < len p ) or ( (len p) + 1 <= i & i < len q ) or i = len p )

proof

assume that
A32: ( not 1 <= i or not i < len p ) and
A33: ( not (len p) + 1 <= i or not i < len q ) ; :: thesis: i = len p
i <= len p by A30, A33, NAT_1:13;
hence i = len p by A29, A32, XXREAL_0:1; :: thesis: verum

end;

A34: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def 3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;
A35: len ((a2 ^ <*x1*>) ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32
.= (len a2) + (len (<*x1*> ^ b1)) by FINSEQ_1:22
.= len (a1 ^ (<*x1*> ^ b1)) by A8, FINSEQ_1:22
.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:32
.= len (the_arity_of o) by A34, FINSEQ_1:6 ;

A36: now :: thesis: for k being Element of NAT st k in dom x holds
x . k in the Sorts of A . ((the_arity_of o) /. k)

let k be Element of NAT ; :: thesis: ( k in dom x implies x . k in the Sorts of A . ((the_arity_of o) /. k) )
assume k in dom x ; :: thesis: x . k in the Sorts of A . ((the_arity_of o) /. k)
then A37: k in Seg (len (the_arity_of o)) by A25, A35, FINSEQ_1:def 3;
then A38: k in dom (the_arity_of o) by FINSEQ_1:def 3;
then A39: k in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def 2;
reconsider dz = dom (the_arity_of o) as non empty set by A37, FINSEQ_1:def 3;
reconsider so = the Sorts of A * (the_arity_of o) as non-empty ManySortedSet of dz ;
A40: not product so is empty ;
pi ((Args (o,A)),k) = pi (((( the Sorts of A #) * the Arity of S) . o),k) by MSUALG_1:def 4
.= pi ((( the Sorts of A #) . ( the Arity of S . o)),k) by FUNCT_2:15
.= pi ((( the Sorts of A #) . (the_arity_of o)),k) by MSUALG_1:def 1
.= pi ((product ( the Sorts of A * (the_arity_of o))),k) by FINSEQ_2:def 5
.= ( the Sorts of A * (the_arity_of o)) . k by A39, A40, CARD_3:12
.= the Sorts of A . ((the_arity_of o) . k) by A38, FUNCT_1:13
.= the Sorts of A . ((the_arity_of o) /. k) by A38, PARTFUN1:def 6 ;
hence x . k in the Sorts of A . ((the_arity_of o) /. k) by CARD_3:def 6; :: thesis: verum

end;

A41: ex i1 being Nat st len p = i1 + 1 by A28, NAT_1:6;

now :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

per cases ( ( 1 <= i & i < len p ) or i = len p or ( (len p) + 1 <= i & i < len q ) ) by A31;

suppose A42: ( 1 <= i & i < len p ) ; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

then A43: i + 1 <= len p by NAT_1:13;
1 <= i + 1 by A42, NAT_1:13;
then i + 1 in dom p by A43, FINSEQ_3:25;
then A44: q . (i + 1) = p . (i + 1) by FINSEQ_1:def 7;
i in dom p by A42, FINSEQ_3:25;
then q . i = p . i by FINSEQ_1:def 7;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A18, A42, A44; :: thesis: verum

end;

suppose A45: i = len p ; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

then i in Seg (len p) by A41, FINSEQ_1:4;
then i in dom p by FINSEQ_1:def 3;
then A46: q . i = (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A17, A45, FINSEQ_1:def 7;
A47: 1 in Seg (len g) by A19, A23, FINSEQ_1:1;
then 1 in dom g by FINSEQ_1:def 3;
then A48: q . (i + 1) = g . 1 by A45, FINSEQ_1:def 7
.= (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A20, A23, A24, A47 ;
for k being Nat st k in dom ((a2 ^ <*x1*>) ^ b1) holds
((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

proof

let k be Nat; :: thesis: ( k in dom ((a2 ^ <*x1*>) ^ b1) implies ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )
assume A49: k in dom ((a2 ^ <*x1*>) ^ b1) ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then A50: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32;

now :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

per cases ( k in dom a2 or ex n1 being Nat st
( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ) by A50, FINSEQ_1:25;

suppose A51: k in dom a2 ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then k in Seg (len a2) by FINSEQ_1:def 3;
then k in dom a1 by A8, FINSEQ_1:def 3;
then A52: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;
((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32
.= a2 . k by A51, FINSEQ_1:def 7 ;
hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A52, ZFMISC_1:87; :: thesis: verum

end;

suppose ex n1 being Nat st
( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then consider n1 being Nat such that
A53: n1 in dom (<*x1*> ^ b1) and
A54: k = (len a2) + n1 ;
((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32
.= (<*x1*> ^ b1) . n1 by A53, A54, FINSEQ_1:def 7
.= (a1 ^ (<*x1*> ^ b1)) . k by A8, A53, A54, FINSEQ_1:def 7
.= x . k by A13, FINSEQ_1:32 ;
hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A25, A36, A49; :: thesis: verum

end;

end;

end;

hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; :: thesis: verum

end;

then reconsider de = (a2 ^ <*x1*>) ^ b1 as Element of Args (o,A) by A35, MSAFREE2:5;
A55: field (C2 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;
field (C1 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;
then field ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) = ( the Sorts of A . (the_result_sort_of o)) \/ ( the Sorts of A . (the_result_sort_of o)) by A55, RELAT_1:18
.= the Sorts of A . (the_result_sort_of o) ;
then A56: (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def 9;
(Den (o,A)) . de in the Sorts of A . (the_result_sort_of o) by A14;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A46, A48, A56, RELAT_2:def 1; :: thesis: verum

end;

suppose A57: ( (len p) + 1 <= i & i < len q ) ; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

then len p < i by NAT_1:13;
then reconsider j = i - (len p) as Element of NAT by NAT_1:21;
A58: 1 <= j + 1 by NAT_1:12;
len f = (len q) - (len p) by A23, A26, XCMPLX_1:26;
then A59: j < len f by A57, XREAL_1:9;
then j + 1 <= len f by NAT_1:13;
then j + 1 in Seg (len f) by A58, FINSEQ_1:1;
then A60: (i + 1) - (len p) in Seg (len f) by XCMPLX_1:29;
A61: 1 <= j by A57, XREAL_1:19;
then A62: [(f . j),(f . (j + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A59;
then A63: f . ((i - (len p)) + 1) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by ZFMISC_1:87;
A64: for k being Nat st k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) holds
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

proof

let k be Nat; :: thesis: ( k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )
assume A65: k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then A66: ( k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) or ex n1 being Nat st
( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;

now :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

per cases ( k in dom a2 or ex n2 being Nat st
( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by A66, FINSEQ_1:25;

suppose A67: k in dom a2 ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then k in Seg (len a2) by FINSEQ_1:def 3;
then k in dom a1 by A8, FINSEQ_1:def 3;
then A68: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . ((i + 1) - (len p)))*> ^ b1)) . k by FINSEQ_1:32
.= a2 . k by A67, FINSEQ_1:def 7 ;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A68, ZFMISC_1:87; :: thesis: verum

end;

suppose ex n2 being Nat st
( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then consider n2 being Nat such that
A69: n2 in dom <*(f . ((i + 1) - (len p)))*> and
A70: k = (len a2) + n2 ;
n2 in Seg 1 by A69, FINSEQ_1:38;
then A71: k = (len a1) + 1 by A8, A70, FINSEQ_1:2, TARSKI:def 1;
then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;
then k in Seg ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:40;
then k in Seg (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:22;
then k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:def 3;
then ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . ((i + 1) - (len p)))*>) . k by FINSEQ_1:def 7
.= f . ((i + 1) - (len p)) by A8, A71, FINSEQ_1:42 ;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A63, A71, XCMPLX_1:29; :: thesis: verum

end;

suppose A72: ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

A73: len (a1 ^ <*x1*>) = (len a1) + (len <*x1*>) by FINSEQ_1:22
.= (len a2) + 1 by A8, FINSEQ_1:40
.= (len a2) + (len <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:40
.= len (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:22 ;
A74: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3
.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40
.= Seg (((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:40
.= Seg ((len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:22
.= Seg (len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1)) by FINSEQ_1:22
.= dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) by FINSEQ_1:def 3 ;
consider n1 being Element of NAT such that
A75: n1 in dom b1 and
A76: k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 by A72;
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = b1 . n1 by A75, A76, FINSEQ_1:def 7
.= x . k by A13, A75, A76, A73, FINSEQ_1:def 7 ;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A65, A74; :: thesis: verum

end;

end;

end;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; :: thesis: verum

end;

A77: f . (i - (len p)) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A62, ZFMISC_1:87;
A78: for k being Nat st k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) holds
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

proof

let k be Nat; :: thesis: ( k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )
assume A79: k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then A80: ( k in dom (a2 ^ <*(f . (i - (len p)))*>) or ex n1 being Nat st
( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;

now :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

per cases ( k in dom a2 or ex n2 being Nat st
( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by A80, FINSEQ_1:25;

suppose A81: k in dom a2 ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then k in Seg (len a2) by FINSEQ_1:def 3;
then k in dom a1 by A8, FINSEQ_1:def 3;
then A82: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . (i - (len p)))*> ^ b1)) . k by FINSEQ_1:32
.= a2 . k by A81, FINSEQ_1:def 7 ;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A82, ZFMISC_1:87; :: thesis: verum

end;

suppose ex n2 being Nat st
( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then consider n2 being Nat such that
A83: n2 in dom <*(f . (i - (len p)))*> and
A84: k = (len a2) + n2 ;
A85: n2 in Seg 1 by A83, FINSEQ_1:38;
then A86: k = (len a1) + 1 by A8, A84, FINSEQ_1:2, TARSKI:def 1;
then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;
then k in Seg ((len a2) + (len <*(f . (i - (len p)))*>)) by FINSEQ_1:40;
then k in Seg (len (a2 ^ <*(f . (i - (len p)))*>)) by FINSEQ_1:22;
then k in dom (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:def 3;
then ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . (i - (len p)))*>) . k by FINSEQ_1:def 7
.= f . (i - (len p)) by A8, A86, FINSEQ_1:42 ;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A8, A77, A84, A85, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

suppose A87: ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

A88: len (a1 ^ <*x1*>) = (len a1) + (len <*x1*>) by FINSEQ_1:22
.= (len a2) + 1 by A8, FINSEQ_1:40
.= (len a2) + (len <*(f . (i - (len p)))*>) by FINSEQ_1:40
.= len (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:22 ;
A89: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3
.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40
.= Seg (((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:40
.= Seg ((len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:22
.= Seg (len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1)) by FINSEQ_1:22
.= dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) by FINSEQ_1:def 3 ;
consider n1 being Element of NAT such that
A90: n1 in dom b1 and
A91: k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 by A87;
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = b1 . n1 by A90, A91, FINSEQ_1:def 7
.= x . k by A13, A90, A91, A88, FINSEQ_1:def 7 ;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A79, A89; :: thesis: verum

end;

end;

end;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; :: thesis: verum

end;

A92: 1 <= j by A57, XREAL_1:19;
j <= len f by A23, A26, A57, XREAL_1:19;
then A93: i - (len p) in Seg (len f) by A92, FINSEQ_1:1;
A94: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def 3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;
A95: len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + 1) + (len b1) by FINSEQ_1:40
.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40
.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22
.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22
.= len (the_arity_of o) by A94, FINSEQ_1:6 ;
len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + 1) + (len b1) by FINSEQ_1:40
.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40
.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22
.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22
.= len (the_arity_of o) by A94, FINSEQ_1:6 ;
then reconsider d1 = (a2 ^ <*(f . (i - (len p)))*>) ^ b1, d2 = (a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1 as Element of Args (o,A) by A78, A64, A95, MSAFREE2:5;
A96: q . i = g . (i - (len p)) by A26, A57, FINSEQ_1:23
.= (Den (o,A)) . d1 by A23, A24, A93 ;
(i + 1) - (len p) = (i - (len p)) + 1 by XCMPLX_1:29;
then A97: [(f . (i - (len p))),(f . ((i + 1) - (len p)))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A61, A59;
A98: i + 1 <= len q by A57, NAT_1:13;
(len p) + 1 <= i + 1 by A57, NAT_1:12;
then q . (i + 1) = g . ((i + 1) - (len p)) by A26, A98, FINSEQ_1:23
.= (Den (o,A)) . d2 by A23, A24, A60 ;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A7, A8, A96, A97, Th12; :: thesis: verum

end;

end;

end;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ; :: thesis: verum

end;

end;

hence [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) by A1, A4, A14, EQREL_1:28; :: thesis: verum