let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 set
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 of 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 set
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 set
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 set
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 set
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 set
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 x1, y1 be set ; :: 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 A2:
( 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) ) )
; :: 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) )
assume that
A3:
[((Den o,A) . ((a1 ^ <*x1*>) ^ b1)),((Den o,A) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o)
and
A4:
[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 A5:
x = (a1 ^ <*x1*>) ^ b1
; :: thesis: [((Den o,A) . x),((Den o,A) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
set y = (a2 ^ <*y1*>) ^ b1;
A7: dom x =
Seg (len ((a1 ^ <*x1*>) ^ b1))
by A5, FINSEQ_1:def 3
.=
Seg (len (a1 ^ (<*x1*> ^ b1)))
by FINSEQ_1:45
.=
Seg ((len a2) + (len (<*x1*> ^ b1)))
by A2, FINSEQ_1:35
.=
Seg (len (a2 ^ (<*x1*> ^ b1)))
by FINSEQ_1:35
.=
Seg (len ((a2 ^ <*x1*>) ^ b1))
by FINSEQ_1:45
.=
dom ((a2 ^ <*x1*>) ^ b1)
by FINSEQ_1:def 3
;
consider C' being ManySortedRelation of the Sorts of A such that
A8:
( C' = C1 \/ C2 & C1 "\/" C2 = EqCl C' )
by Def4;
A9: (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 Th2
.=
EqCl (C' . (the_result_sort_of o))
by A8, PBOOLE:def 7
.=
(C1 "\/" C2) . (the_result_sort_of o)
by A8, Def3
;
A10: the Sorts of A . (the_result_sort_of o) =
the Sorts of A . (the ResultSort of S . o)
by MSUALG_1:def 7
.=
(the Sorts of A * the ResultSort of S) . o
by FUNCT_2:21
.=
Result o,A
by MSUALG_1:def 10
;
then
(Den o,A) . x in the Sorts of A . (the_result_sort_of o)
;
then consider p being FinSequence such that
A11:
( 1 <= len p & (Den o,A) . ((a1 ^ <*x1*>) ^ b1) = p . 1 & (Den o,A) . ((a2 ^ <*x1*>) ^ b1) = p . (len p) & ( for i being Element of 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, A3, A5, A9, EQREL_1:36;
consider D' being ManySortedRelation of the Sorts of A such that
A12:
( D' = C1 \/ C2 & C1 "\/" C2 = EqCl D' )
by Def4;
A13: (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 Th2
.=
EqCl (D' . ((the_arity_of o) /. (n + 1)))
by A12, PBOOLE:def 7
.=
(C1 "\/" C2) . ((the_arity_of o) /. (n + 1))
by A12, Def3
;
x1 in the Sorts of A . ((the_arity_of o) /. (n + 1))
by A4, ZFMISC_1:106;
then consider f being FinSequence such that
A14:
( 1 <= len f & x1 = f . 1 & y1 = f . (len f) & ( for i being Element of 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, A4, A13, EQREL_1:36;
deffunc H1( Nat) -> set = (Den o,A) . ((a2 ^ <*(f . $1)*>) ^ b1);
consider g being FinSequence such that
A15:
( len g = len f & ( for i being Nat st i in dom g holds
g . i = H1(i) ) )
from FINSEQ_1:sch 2();
A16:
dom g = Seg (len f)
by A15, 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 Element of 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 Element of 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)) ) )
A17:
len q = (len p) + (len g)
by FINSEQ_1:35;
hence
1
<= len q
by A11, NAT_1:12;
:: thesis: ( (Den o,A) . x = q . 1 & (Den o,A) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of 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 A11, FINSEQ_3:27;
hence
q . 1
= (Den o,A) . x
by A5, A11, FINSEQ_1:def 7;
:: thesis: ( (Den o,A) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of 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)) ) )
A18:
len g in Seg (len f)
by A14, A15, FINSEQ_1:3;
then
len g in dom g
by A15, FINSEQ_1:def 3;
hence q . (len q) =
g . (len g)
by A17, FINSEQ_1:def 7
.=
(Den o,A) . ((a2 ^ <*y1*>) ^ b1)
by A14, A15, A18, A16
;
:: thesis: for i being Element of 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))
A19:
len p <> 0
by A11;
hereby :: thesis: verum
let i be
Element of
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 A20:
( 1
<= i &
i < len q )
;
:: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))A21:
( ( 1
<= i &
i < len p ) or (
(len p) + 1
<= i &
i < len q ) or
i = len p )
consider i1 being
Nat such that A24:
len p = i1 + 1
by A19, NAT_1:6;
A25:
Seg (len ((a1 ^ <*x1*>) ^ b1)) =
dom x
by A5, FINSEQ_1:def 3
.=
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
A26:
len ((a2 ^ <*x1*>) ^ b1) =
len (a2 ^ (<*x1*> ^ b1))
by FINSEQ_1:45
.=
(len a2) + (len (<*x1*> ^ b1))
by FINSEQ_1:35
.=
len (a1 ^ (<*x1*> ^ b1))
by A2, FINSEQ_1:35
.=
len ((a1 ^ <*x1*>) ^ b1)
by FINSEQ_1:45
.=
len (the_arity_of o)
by A25, FINSEQ_1:8
;
A27:
now 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 A28:
k in Seg (len (the_arity_of o))
by A7, A26, FINSEQ_1:def 3;
then A29:
k in dom (the_arity_of o)
by FINSEQ_1:def 3;
then A30:
k in dom (the Sorts of A * (the_arity_of o))
by PARTFUN1:def 4;
reconsider dz =
dom (the_arity_of o) as non
empty set by A28, FINSEQ_1:def 3;
reconsider so = the
Sorts of
A * (the_arity_of o) as
V2()
ManySortedSet of ;
A31:
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 9
.=
pi ((the Sorts of A # ) . (the Arity of S . o)),
k
by FUNCT_2:21
.=
pi ((the Sorts of A # ) . (the_arity_of o)),
k
by MSUALG_1:def 6
.=
pi (product (the Sorts of A * (the_arity_of o))),
k
by PBOOLE:def 19
.=
(the Sorts of A * (the_arity_of o)) . k
by A30, A31, CARD_3:22
.=
the
Sorts of
A . ((the_arity_of o) . k)
by A29, FUNCT_1:23
.=
the
Sorts of
A . ((the_arity_of o) /. k)
by A29, PARTFUN1:def 8
;
hence
x . k in the
Sorts of
A . ((the_arity_of o) /. k)
by CARD_3:def 6;
:: thesis: verum end; now per cases
( ( 1 <= i & i < len p ) or i = len p or ( (len p) + 1 <= i & i < len q ) )
by A21;
suppose A34:
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 A24, FINSEQ_1:6;
then
i in dom p
by FINSEQ_1:def 3;
then A35:
q . i = (Den o,A) . ((a2 ^ <*x1*>) ^ b1)
by A11, A34, FINSEQ_1:def 7;
A36:
1
in Seg (len g)
by A14, A15, FINSEQ_1:3;
then
1
in dom g
by FINSEQ_1:def 3;
then A37:
q . (i + 1) =
g . 1
by A34, FINSEQ_1:def 7
.=
(Den o,A) . ((a2 ^ <*x1*>) ^ b1)
by A14, A15, A36, A16
;
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)
then reconsider de =
(a2 ^ <*x1*>) ^ b1 as
Element of
Args o,
A by A26, MSAFREE2:7;
A43:
(Den o,A) . de in the
Sorts of
A . (the_result_sort_of o)
by A10;
(
field (C1 . (the_result_sort_of o)) = the
Sorts of
A . (the_result_sort_of o) &
field (C2 . (the_result_sort_of o)) = the
Sorts of
A . (the_result_sort_of o) )
by EQREL_1:16;
then A44:
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 RELAT_1:33
.=
the
Sorts of
A . (the_result_sort_of o)
;
(C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) is
reflexive
by RELAT_2:31;
then
(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 A44, RELAT_2:def 9;
hence
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
by A35, A37, A43, RELAT_2:def 1;
:: thesis: verum end; suppose A45:
(
(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 A46:
(len p) + 1
<= i + 1
by NAT_1:12;
A47:
i + 1
<= len q
by A45, NAT_1:13;
len p < i
by A45, NAT_1:13;
then reconsider j =
i - (len p) as
Element of
NAT by NAT_1:21;
A48:
1
<= j
by A45, XREAL_1:21;
len f = (len q) - (len p)
by A15, A17, XCMPLX_1:26;
then A49:
j < len f
by A45, XREAL_1:11;
( 1
<= j &
j <= len f )
by A15, A17, A45, XREAL_1:21;
then A51:
i - (len p) in Seg (len f)
by FINSEQ_1:3;
( 1
<= j + 1 &
j + 1
<= len f )
by A49, NAT_1:12, NAT_1:13;
then
j + 1
in Seg (len f)
by FINSEQ_1:3;
then A53:
(i + 1) - (len p) in Seg (len f)
by XCMPLX_1:29;
A55:
[(f . j),(f . (j + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1)))
by A14, A48, A49;
then A56:
f . (i - (len p)) in the
Sorts of
A . ((the_arity_of o) /. (n + 1))
by ZFMISC_1:106;
A57:
f . ((i - (len p)) + 1) in the
Sorts of
A . ((the_arity_of o) /. (n + 1))
by A55, ZFMISC_1:106;
A58:
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 A59:
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 A60:
(
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:38;
now 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 A60, FINSEQ_1:38;
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 A63:
(
n2 in dom <*(f . (i - (len p)))*> &
k = (len a2) + n2 )
;
A64:
n2 in Seg 1
by A63, FINSEQ_1:55;
then A65:
k = (len a1) + 1
by A2, A63, FINSEQ_1:4, TARSKI:def 1;
then
k in Seg ((len a2) + 1)
by A2, FINSEQ_1:6;
then
k in Seg ((len a2) + (len <*(f . (i - (len p)))*>))
by FINSEQ_1:57;
then
k in Seg (len (a2 ^ <*(f . (i - (len p)))*>))
by FINSEQ_1:35;
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 A2, A65, FINSEQ_1:59
;
hence
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the
Sorts of
A . ((the_arity_of o) /. k)
by A2, A56, A63, A64, FINSEQ_1:4, TARSKI:def 1;
:: thesis: verum end;
hence
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the
Sorts of
A . ((the_arity_of o) /. k)
;
:: thesis: verum
end; A69:
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 A70:
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 A71:
(
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:38;
now 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 A71, FINSEQ_1:38;
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 A74:
(
n2 in dom <*(f . ((i + 1) - (len p)))*> &
k = (len a2) + n2 )
;
n2 in Seg 1
by A74, FINSEQ_1:55;
then A75:
k = (len a1) + 1
by A2, A74, FINSEQ_1:4, TARSKI:def 1;
then
k in Seg ((len a2) + 1)
by A2, FINSEQ_1:6;
then
k in Seg ((len a2) + (len <*(f . ((i + 1) - (len p)))*>))
by FINSEQ_1:57;
then
k in Seg (len (a2 ^ <*(f . ((i + 1) - (len p)))*>))
by FINSEQ_1:35;
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 A2, A75, FINSEQ_1:59
;
hence
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the
Sorts of
A . ((the_arity_of o) /. k)
by A2, A57, A75, XCMPLX_1:29;
:: thesis: verum end;
hence
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the
Sorts of
A . ((the_arity_of o) /. k)
;
:: thesis: verum
end; A79:
Seg (len ((a1 ^ <*x1*>) ^ b1)) =
dom x
by A5, FINSEQ_1:def 3
.=
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
(
len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) = len (the_arity_of o) &
len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) = len (the_arity_of o) )
then reconsider d1 =
(a2 ^ <*(f . (i - (len p)))*>) ^ b1,
d2 =
(a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1 as
Element of
Args o,
A by A58, A69, MSAFREE2:7;
A80:
q . i =
g . (i - (len p))
by A17, A45, FINSEQ_1:36
.=
(Den o,A) . d1
by A15, A51, A16
;
A81:
q . (i + 1) =
g . ((i + 1) - (len p))
by A17, A46, A47, FINSEQ_1:36
.=
(Den o,A) . d2
by A15, A53, A16
;
(i + 1) - (len p) = (i - (len p)) + 1
by XCMPLX_1:29;
then
[(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 A14, A48, A49;
hence
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
by A2, A80, A81, Th14;
:: thesis: verum 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, A9, A10, EQREL_1:36; :: thesis: verum