let S be non empty non void ManySortedSign ; 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; 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; 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; 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; ( 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
; 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 ; 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 ; 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; ( 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)
; ( 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))
; 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); ( 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
; [((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 H1( 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 = H1(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;
( 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;
( (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;
( (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
;
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 verum
let i be
Nat;
( 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
;
[(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 )
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 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 ;
( k in dom x implies x . k in the Sorts of A . ((the_arity_of o) /. k) )assume
k in dom x
;
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
V2()
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;
verum end; A41:
ex
i1 being
Nat st
len p = i1 + 1
by A28, NAT_1:6;
now [(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 A45:
i = len p
;
[(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)
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;
verum end; suppose A57:
(
(len p) + 1
<= i &
i < len q )
;
[(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;
( 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)
;
((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 ((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
ex
n2 being
Nat st
(
n2 in dom <*(f . ((i + 1) - (len p)))*> &
k = (len a2) + n2 )
;
((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;
verum end; suppose A72:
ex
n1 being
Element of
NAT st
(
n1 in dom b1 &
k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 )
;
((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;
verum end; end; end;
hence
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the
Sorts of
A . ((the_arity_of o) /. k)
;
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;
( 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)
;
((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 ((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
ex
n2 being
Nat st
(
n2 in dom <*(f . (i - (len p)))*> &
k = (len a2) + n2 )
;
((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;
verum end; suppose A87:
ex
n1 being
Element of
NAT st
(
n1 in dom b1 &
k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 )
;
((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;
verum end; end; end;
hence
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the
Sorts of
A . ((the_arity_of o) /. k)
;
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;
verum end; end; end; hence
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
;
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; verum