let S be non empty non void ManySortedSign ; :: thesis:
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis:
let v be Element of (Free (S,Y)); :: thesis:
let h be Endomorphism of Free (S,Y); :: thesis:
let f be vf-sequence of v; :: thesis:
assume A0: f <> {} ; :: thesis:
then ( {} <> dom f & dom f = dom (pr2 f) ) by MCART_1:def 13;
then reconsider B = pr2 f as non empty FinSequence of the carrier of S by Th96;
consider g being one-to-one FinSequence such that
AA: ( rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom f = dom g & ( for i being Nat st i in dom f holds
f . i = v . (g . i) ) ) by VFS;
rng g c= dom v

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng g ; :: thesis:
then ex xi being Element of dom v st
( a = xi & ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] ) by AA;
hence a in dom v ; :: thesis:

end;

then reconsider g = g as one-to-one FinSequence of dom v by FINSEQ_1:def 4;
take B ; :: thesis:
B = pr2 f ;
then reconsider V1 = pr1 f as B -sorts FinSequence of Union Y by Th97;
take V1 ; :: thesis:
thus AB: ( dom B = dom f & B = pr2 f & V1 = pr1 f ) by MCART_1:def 13; :: thesis:
deffunc H₁( Element of dom B) -> Element of (Free (S,Y)) = h . ((V1 . $1) -term);
consider D being non empty FinSequence such that
A2: ( dom D = dom B & ( for i being Element of dom B holds D . i = H₁(i) ) ) from MSAFREE5:sch 6();
D is FinSequence of (Free (S,Y))

proof

let a be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis:
assume a in rng D ; :: thesis:
then consider b being object such that
A3: ( b in dom D & a = D . b ) by FUNCT_1:def 3;
reconsider b = b as Element of dom B by A2, A3;
a = H₁(b) by A2, A3;
hence a in Union the Sorts of (Free (S,Y)) ; :: thesis:

end;

then reconsider D = D as FinSequence of (Free (S,Y)) ;
D is B -sorts

proof

thus dom D = dom B by A2; :: according to MSAFREE5:def 37 :: thesis:
let i be Nat; :: thesis:
assume i in dom B ; :: thesis:
then reconsider i = i as Element of dom B ;
reconsider t = (V1 . i) -term as Element of (Free (S,Y)) ;
the_sort_of t = B . i by SORT;
then the_sort_of (h . t) = B . i by Lem0;
then h . t in the Sorts of (Free (S,Y)) . (B . i) by SORT;
hence D . i in the Sorts of (Free (S,Y)) . (B . i) by A2; :: thesis:

end;

then reconsider D = D as B -sorts FinSequence of (Free (S,Y)) ;
take D ; :: thesis:
set V2 = the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y;
take the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y ; :: thesis:
thus for i being Element of dom B holds D . i = h . ((V1 . i) -term) by A2; :: thesis:
deffunc H₂( Element of dom B, DecoratedTree) -> set = ($2 with-replacement ((g /. $1),(D . $1))) with-replacement ((g /. ($1 + 1)),(root-tree [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . ($1 + 1)),(B . ($1 + 1))]));
consider F being non empty DTree-yielding FinSequence such that
A7: ( dom F = dom B & F . 1 = v with-replacement ((g /. 1),(root-tree [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)])) & ( for i, j being Element of dom B st j = i + 1 holds
for d being DecoratedTree st d = F . i holds
F . j = H₂(i,d) ) ) from MSAFREE5:sch 8();
rng F c= Union the Sorts of (Free (S,Y))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
then consider b being object such that
B1: ( b in dom F & a = F . b ) by FUNCT_1:def 3;
reconsider b = b as Element of dom B by A7, B1;
defpred S₁[ Nat] means ( $1 in dom B implies ( F . $1 in Union the Sorts of (Free (S,Y)) & g . $1 in dom (F . $1) & (F . $1) . (g . $1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . $1),(B . $1)] & ( for j being Nat st j > $1 & j in dom B holds
( g . j in dom (F . $1) & (F . $1) . (g . j) = [(V1 . j),(B . j)] ) ) ) );
B2: S₁[1]

proof

assume 1 in dom B ; :: thesis:
then reconsider b = 1 as Element of dom B ;
reconsider bb = b as Element of dom g by AA, MCART_1:def 13;
g . b in rng g by AA, AB, FUNCT_1:def 3;
then consider xi being Element of dom v such that
B3: ( g . b = xi & ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] ) by AA;
consider s being SortSymbol of S, y being Element of Y . s such that
B4: v . xi = [y,s] by B3;
reconsider v2 = ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term as Element of (Free (S,Y)) ;
f . b = v . (g . b) by AA, AB;
then ( V1 . b = [y,s] `1 & B . b = [y,s] `2 ) by B3, B4, AB, MCART_1:def 12, MCART_1:def 13;
then B6: ( v . (g . b) = [(V1 . b),(B . b)] & the_sort_of v2 = B . b ) by B3, B4, SORT;
B7: g /. bb = g . bb by AA, A0, PARTFUN1:def 6;
F . b is Element of (Free (S,Y)),(the_sort_of v) by A7, B6, B7, Th117;
hence F . 1 in Union the Sorts of (Free (S,Y)) ; :: thesis:
C1: dom (F . b) = (dom v) with-replacement ((g /. bb),(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) by B3, B7, A7, TREES_2:def 11;
hence g . 1 in dom (F . 1) by B3, B7, TREES_1:def 9; :: thesis:
then consider r being FinSequence of NAT such that
CD: ( r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) & xi = xi ^ r & (F . b) . xi = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r ) by C1, A7, B7, B3, TREES_2:def 11;
r = {} by CD, FINSEQ_1:87;
hence (F . 1) . (g . 1) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . 1),(B . 1)] by CD, B3, TREES_4:3; :: thesis:
let j be Nat; :: thesis:
assume C2: ( j > 1 & j in dom B ) ; :: thesis:
then g . j in rng g by AA, AB, FUNCT_1:def 3;
then consider xi2 being Element of dom v such that
C3: ( g . j = xi2 & ex s being SortSymbol of S ex y being Element of Y . s st v . xi2 = [y,s] ) by AA;
consider s being SortSymbol of S, y being Element of Y . s such that
C4: v . xi2 = [y,s] by C3;
f . j = v . (g . j) by C2, AA, AB;
then B0: ( V1 . j = [y,s] `1 & B . j = [y,s] `2 ) by C3, C4, C2, AB, MCART_1:def 12, MCART_1:def 13;
xi <> xi2 by AA, AB, C2, C3, B3, FUNCT_1:def 4;
then C6: not xi c= xi2 by B4, Lem9;
then C8: for r being FinSequence of NAT holds
( not r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not xi2 = xi ^ r or not (v with-replacement ((g /. bb),(( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) . xi2 = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r ) by TREES_1:1;
C7: ( not xi c< xi2 & dom (F . b) = (dom v) with-replacement (xi,(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) ) by A7, B3, C6, B7, TREES_2:def 11, XBOOLE_0:def 8;
hence g . j in dom (F . 1) by C3, TREES_1:def 9; :: thesis:
hence (F . 1) . (g . j) = [(V1 . j),(B . j)] by C7, C8, B3, B7, A7, B0, C3, C4, TREES_2:def 11; :: thesis:

end;

B8: for i being Nat st i >= 1 & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume Z1: i >= 1 ; :: thesis:
assume Z2: S₁[i] ; :: thesis:
assume Z3: i + 1 in dom B ; :: thesis:
then i + 1 <= len B by FINSEQ_3:25;
then D0: i < len B by NAT_1:13;
then D1: ( i in dom B & i + 1 > i ) by Z1, NAT_1:13, FINSEQ_3:25;
reconsider v1 = F . i as Element of (Free (S,Y)) by Z2, D0, Z1, FINSEQ_3:25;
reconsider b = i, b1 = i + 1 as Element of dom B by D0, Z3, Z1, FINSEQ_3:25;
D2: ( g . (i + 1) in dom v1 & v1 . (g . (i + 1)) = [(V1 . b1),(B . b1)] ) by D1, Z2, Z3;
D3: ( g . b in dom v1 & v1 . (g . b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] ) by Z2;
reconsider xi1 = g . b, xi2 = g . (i + 1) as Element of dom v1 by Z2, D1, Z3;
D4: ( g /. b = xi1 & g /. b1 = xi2 ) by AA, AB, PARTFUN1:def 6;
the_sort_of (D . b) = B . b by SORT;
then reconsider v2 = v1 with-replacement (xi1,(D . b)) as Element of (Free (S,Y)),(the_sort_of v1) by D3, Th117;
xi1 <> xi2 by AA, AB, Z3, D1, FUNCT_1:def 4;
then D5: not xi1 c= xi2 by D3, Lem9;
then D6: for r being FinSequence of NAT holds
( not r in dom (D . b) or not xi2 = xi1 ^ r or not v2 . xi2 = (D . b) . r ) by TREES_1:1;
reconsider t1 = ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1) -term as Element of (Free (S,Y)) ;
not xi1 c< xi2 by D5, XBOOLE_0:def 8;
then DD: xi2 in (dom v1) with-replacement (xi1,(dom (D . b))) by TREES_1:def 9;
then D7: ( xi2 in dom v2 & v2 . xi2 = [(V1 . b1),(B . b1)] & the_sort_of t1 = B . b1 ) by D6, D2, SORT, TREES_2:def 11;
reconsider xi3 = xi2 as Element of dom v2 by DD, TREES_2:def 11;
reconsider v3 = v2 with-replacement (xi3,t1) as Element of (Free (S,Y)),(the_sort_of v2) by D7, Th117;
D8: F . (i + 1) = v3 by D4, A7;
hence F . (i + 1) in Union the Sorts of (Free (S,Y)) ; :: thesis:
D9: dom (F . b1) = (dom v2) with-replacement (xi3,(dom t1)) by D8, TREES_2:def 11;
thus g . (i + 1) in dom (F . (i + 1)) by D9, TREES_1:def 9; :: thesis:
then consider r being FinSequence of NAT such that
D10: ( r in dom t1 & xi3 = xi3 ^ r & v3 . xi3 = t1 . r ) by D9, TREES_2:def 11;
r = {} by D10, FINSEQ_1:87;
hence (F . (i + 1)) . (g . (i + 1)) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (i + 1)),(B . (i + 1))] by D8, D10, TREES_4:3; :: thesis:
let j be Nat; :: thesis:
assume E1: ( j > i + 1 & j in dom B ) ; :: thesis:
then reconsider b2 = j as Element of dom B ;
EE: j > i by E1, NAT_1:13;
then E2: ( g . j in dom v1 & v1 . (g . j) = [(V1 . b2),(B . b2)] ) by E1, Z2, D0, Z1, FINSEQ_3:25;
reconsider xi = g . j as Element of dom v1 by EE, E1, Z2, D0, Z1, FINSEQ_3:25;
xi1 <> xi by E1, AA, AB, D1, FUNCT_1:def 4;
then E5: not xi1 c= xi by D3, Lem9;
then E6: for r being FinSequence of NAT holds
( not r in dom (D . b) or not xi = xi1 ^ r or not v2 . xi = (D . b) . r ) by TREES_1:1;
reconsider t2 = ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b2) -term as Element of (Free (S,Y)) ;
not xi1 c< xi by E5, XBOOLE_0:def 8;
then EF: xi in (dom v1) with-replacement (xi1,(dom (D . b))) by TREES_1:def 9;
then E7: ( xi in dom v2 & v2 . xi = [(V1 . b2),(B . b2)] & the_sort_of t2 = B . b2 ) by E6, E2, SORT, TREES_2:def 11;
reconsider xi = xi as Element of dom v2 by EF, TREES_2:def 11;
xi3 <> xi by AA, AB, Z3, E1, FUNCT_1:def 4;
then E9: not xi3 c= xi by Lem9, D2;
then not xi3 c< xi by XBOOLE_0:def 8;
hence E8: g . j in dom (F . (i + 1)) by D9, TREES_1:def 9; :: thesis:
for r being FinSequence of NAT holds
( not r in dom t1 or not xi = xi3 ^ r or not v3 . xi = t1 . r ) by E9, TREES_1:1;
hence (F . (i + 1)) . (g . j) = [(V1 . j),(B . j)] by E7, D8, D9, E8, TREES_2:def 11; :: thesis:

end;

B9: for i being Nat st i >= 1 holds
S₁[i] from NAT_1:sch 8(B2, B8);
b >= 1 by FINSEQ_3:25;
hence a in Union the Sorts of (Free (S,Y)) by B1, B9; :: thesis:

end;

then reconsider F = F as FinSequence of (Free (S,Y)) by FINSEQ_1:def 4;
defpred S₁[ Nat] means for b being Element of dom B st $1 = b holds
( F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b & dom v c= dom (F . b) & (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & ( for b1 being Element of dom B st b1 > b holds
( F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] ) ) );
F1: S₁[1]

proof

let b be Element of dom B; :: thesis:
assume F2: 1 = b ; :: thesis:
reconsider xi = g /. b as Element of dom v ;
reconsider t = ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term as Element of (Free (S,Y)) ;
reconsider F1 = F . 1 as Element of (Free (S,Y)) by A7, F2, FUNCT_1:102;
F3: F1 = v with-replacement (xi,t) by A7, F2;
FD: dom F1 = (dom v) with-replacement (xi,(dom t)) by A7, F2, TREES_2:def 11;
v is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b -omitting

proof

end;

hence F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b by F2, F3, Lem10; :: thesis:
g . b = xi by AA, AB, PARTFUN1:def 6;
then xi in rng g by AA, AB, FUNCT_1:def 3;
then consider nu being Element of dom v such that
G0: ( xi = nu & ex s being SortSymbol of S ex y being Element of Y . s st v . nu = [y,s] ) by AA;
thus dom v c= dom (F . b) by G0, F2, F3, Lem11; :: thesis:
then ( xi ^ {} = xi & xi in dom F1 ) by F2;
then consider mu being FinSequence of NAT such that
H0: ( mu in dom t & xi = xi ^ mu & F1 . xi = t . mu ) by A7, F2, FD, TREES_2:def 11;
mu = {} by H0, FINSEQ_1:87;
hence (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] by F2, H0, TREES_4:3; :: thesis:
let b1 be Element of dom B; :: thesis:
assume G1: b1 > b ; :: thesis:
thus F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting :: thesis:

proof

assume Coim ((F /. b),[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]) <> {} ; :: according to MSAFREE5:def 21 :: thesis:
then consider i being object such that
G2: i in Coim ((F /. b),[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]) by XBOOLE_0:7;
G3: ( i in dom (F /. b) & (F /. b) . i in {[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]} ) by G2, FUNCT_1:def 7;
reconsider i = i as Element of dom (F /. b) by G2, FUNCT_1:def 7;
G4: F /. b = F . b by A7, PARTFUN1:def 6;
G5: (F /. b) . i = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)] by G3, TARSKI:def 1;
G7: dom F1 = (dom v) with-replacement (xi,(dom t)) by A7, F2, TREES_2:def 11;

per cases by F2, A7, G4, TREES_2:def 11;

suppose G6: ( not xi is_a_prefix_of i & F1 . i = v . i ) ; :: thesis:

then for r being FinSequence of NAT holds
( not r in dom t or not i = xi ^ r ) by TREES_1:1;
then i is Element of dom v by G4, G7, F2, TREES_1:def 9;
then i in rng g by AA, G5, G6, G4, F2;
then consider j being object such that
G8: ( j in dom g & g . j = i ) by FUNCT_1:def 3;
reconsider j = j as Element of dom B by AA, G8, MCART_1:def 13;
f . j = v . (g . j) by AA, AB;
then ( V1 . j = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)] `1 & dom V1 = dom B ) by AB, G8, G6, G5, G4, F2, MCART_1:def 12;
then ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 in rng V1 & rng V1 misses rng the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y ) by OMIT2, FUNCT_1:def 3;
then ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 nin rng the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y & dom the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y = dom B ) by SORTS, XBOOLE_0:3;
hence contradiction by FUNCT_1:def 3; :: thesis:

end;

suppose ex r being FinSequence of NAT st
( r in dom t & i = xi ^ r & F1 . i = t . r ) ; :: thesis:

then consider r being FinSequence of NAT such that
G9: ( r in dom t & i = xi ^ r & F1 . i = t . r ) ;
r in {{}} by G9, TREES_1:29;
then r = {} ;
then G10: ( F1 . i = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & dom the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y = dom B ) by G9, SORTS, TREES_4:3;
then the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b <> the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 by G1, FUNCT_1:def 4;
hence contradiction by G5, G4, F2, G10, XTUPLE_0:1; :: thesis:

end;

K2: ( xi = g . b & g /. b1 = g . b1 ) by AA, AB, PARTFUN1:def 6;
then K0: ( v . xi = f . b & v . (g /. b1) = f . b1 & g /. b1 in rng g & xi in rng g ) by AA, AB, FUNCT_1:def 3;
then consider mu being Element of dom v such that
K1: ( mu = g /. b1 & ex s being SortSymbol of S ex y being Element of Y . s st v . mu = [y,s] ) by AA;
reconsider fb1 = f . b1 as pair object by K2, K1, AA, AB;
K3: v . mu = [(fb1 `1),(fb1 `2)] by K2, K1, AA, AB
.= [(V1 . b1),(fb1 `2)] by AB, MCART_1:def 12
.= [(V1 . b1),(B . b1)] by AB, MCART_1:def 13 ;
consider nu being Element of dom v such that
K4: ( nu = xi & ex s being SortSymbol of S ex y being Element of Y . s st v . nu = [y,s] ) by AA, K0;
reconsider fb = f . b as pair object by K2, K4, AA, AB;
K5: v . xi = [(fb `1),(fb `2)] by K2, AA, AB
.= [(V1 . b),(fb `2)] by AB, MCART_1:def 12
.= [(V1 . b),(B . b)] by AB, MCART_1:def 13 ;
xi <> mu by AA, AB, K1, K2, G1, FUNCT_1:def 4;
then K6: not xi c= mu by K5, Lem9;
then not xi c< mu by XBOOLE_0:def 8;
then K7: mu in (dom v) with-replacement (xi,(dom t)) by TREES_1:def 9;
for r being FinSequence of NAT holds
( not r in dom t or not mu = xi ^ r or not F1 . mu = t . r ) by K6, TREES_1:1;
hence (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] by F2, A7, K1, K3, K7, TREES_2:def 11; :: thesis:

end;

WW: for i being Nat st 1 <= i & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume H1: ( 1 <= i & S₁[i] ) ; :: thesis:
let b be Element of dom B; :: thesis:
assume H2: i + 1 = b ; :: thesis:
reconsider xi = g /. b as Element of dom v ;
reconsider t = ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term as Element of (Free (S,Y)) ;
i + 1 <= len F by A7, H2, FINSEQ_3:25;
then HH: ( 1 <= i & i < len F ) by H1, NAT_1:13;
reconsider F1 = F . (i + 1), Fi = F . i as Element of (Free (S,Y)) by HH, A7, H2, FUNCT_1:102, FINSEQ_3:25;
reconsider bi = i as Element of dom B by HH, A7, FINSEQ_3:25;
reconsider Fi = Fi as context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . bi by H1;
reconsider nu = g /. bi as Element of dom v ;
F3: F1 = (Fi with-replacement (nu,(D . bi))) with-replacement (xi,t) by A7, H2;
H8: ( b > bi & F /. bi = Fi ) by A7, H2, NAT_1:13, PARTFUN1:def 6;
then H5: ( Fi is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b -omitting & Fi . xi = [(V1 . b),(B . b)] ) by H1;
I2: ( D . bi in the Sorts of (Free (S,Y)) . (B . bi) & dom v c= dom Fi ) by H1;
( nu = g . bi & xi = g . b ) by AA, AB, PARTFUN1:def 6;
then H6: ( Fi . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . bi),(B . bi)] & the_sort_of (D . bi) = B . bi & nu in dom Fi & xi in dom Fi & nu <> xi ) by AA, AB, I2, H1, H8, SORT, FUNCT_1:def 4;
then H7: Fi with-replacement (nu,(D . bi)) = Fi -sub (D . bi) by Th118;
I1: not nu c= xi by H6, Lem9;
then not nu c< xi by XBOOLE_0:def 8;
then I3: xi in (dom Fi) with-replacement (nu,(dom (D . bi))) by H6, TREES_1:def 9;
then H9: xi in dom (Fi -sub (D . bi)) by H6, H7, TREES_2:def 11;
D . bi is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b -omitting by OMIT4;
then Fi -sub (D . bi) is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b -omitting by H5, H6, Th45A;
hence F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b by H2, F3, H7, H9, Lem10; :: thesis:
for r being FinSequence of NAT holds
( not r in dom (D . bi) or not xi = nu ^ r or not (Fi with-replacement (nu,(D . bi))) . xi = (D . bi) . r ) by I1, TREES_1:1;
then (Fi -sub (D . bi)) . xi = [(V1 . b),(B . b)] by I3, H5, H6, H7, TREES_2:def 11;
then L1: ( dom Fi c= dom (Fi -sub (D . bi)) & dom (Fi -sub (D . bi)) c= dom F1 ) by F3, H7, H9, H6, Lem11;
hence dom v c= dom (F . b) by I2, H2; :: thesis:
( xi in dom F1 & dom F1 = (dom (Fi -sub (D . bi))) with-replacement (xi,(dom t)) ) by L1, F3, H7, H6, TREES_2:def 11;
then consider r being FinSequence of NAT such that
J0: ( r in dom t & xi = xi ^ r & F1 . xi = t . r ) by H7, H9, F3, TREES_2:def 11;
r = {} by J0, FINSEQ_1:87;
hence (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] by H2, J0, TREES_4:3; :: thesis:
let b1 be Element of dom B; :: thesis:
assume J1: b1 > b ; :: thesis:
thus F /. b is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting :: thesis:

proof

assume Coim ((F /. b),[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]) <> {} ; :: according to MSAFREE5:def 21 :: thesis:
then consider a being object such that
J2: a in Coim ((F /. b),[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]) by XBOOLE_0:7;
J3: ( a in dom (F /. b) & (F /. b) . a in {[( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1),(B . b1)]} ) by J2, FUNCT_1:def 7;
reconsider q = a as Element of dom (F /. b) by J2, FUNCT_1:def 7;
J4: F /. b = F . b by A7, PARTFUN1:def 6;
then J5: ( q in (dom (Fi -sub (D . bi))) with-replacement (xi,(dom t)) & (dom (Fi -sub (D . bi))) with-replacement (xi,(dom t)) = dom F1 ) by F3, J3, H2, H7, H9, TREES_2:def 11;

per cases by F3, H7, H9, TREES_2:def 11;

suppose J6: ( not xi is_a_prefix_of q & F1 . q = (Fi -sub (D . bi)) . q ) ; :: thesis:

then J7: q in dom (Fi -sub (D . bi)) by H9, J5, Th01;
b1 > bi by J1, H2, NAT_1:13;
then ( Fi is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting & D . bi is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting ) by H1, H8, OMIT4;
then Fi -sub (D . bi) is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting by H6, Th45A;
hence contradiction by J7, H2, J3, J4, J6, FUNCT_1:def 7; :: thesis:

end;

suppose ex r being FinSequence of NAT st
( r in dom t & q = xi ^ r & F1 . q = t . r ) ; :: thesis:

then consider r being FinSequence of NAT such that
J8: ( r in dom t & q = xi ^ r & F1 . q = t . r ) ;
dom the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y = dom B by SORTS;
then the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b <> the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 by J1, FUNCT_1:def 4;
then t is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b1 -omitting by ThC1;
hence contradiction by H2, J3, J4, J8, FUNCT_1:def 7; :: thesis:

end;

reconsider mu = g /. b1 as Node of v ;
L5: ( bi < b1 & b > bi ) by J1, H2, NAT_1:13;
then L2: ( Fi . (g /. b1) = [(V1 . b1),(B . b1)] & Fi . (g /. b) = [(V1 . b),(B . b)] ) by H1;
( g /. b1 = g . b1 & g /. b = g . b & g /. bi = g . bi ) by AA, AB, PARTFUN1:def 6;
then ( g /. b1 <> g /. b & g /. bi <> g /. b1 & g /. b1 in dom Fi & g /. b in dom Fi & g /. bi in dom Fi ) by AB, AA, J1, I2, L5, FUNCT_1:def 4;
then L3: ( not g /. b c= g /. b1 & not nu c= mu ) by H6, L2, Lem9;
then L4: for r being FinSequence of NAT holds
( not r in dom (D . bi) or not mu = nu ^ r or not (Fi -sub (D . bi)) . mu = (D . bi) . r ) by TREES_1:1;
L6: ( nu in dom Fi & g /. b1 in dom (Fi -sub (D . bi)) ) by I2, L1;
then g /. b1 in (dom Fi) with-replacement (nu,(dom (D . bi))) by H7, TREES_2:def 11;
then L7: (Fi -sub (D . bi)) . (g /. b1) = [(V1 . b1),(B . b1)] by L4, L2, L6, H7, TREES_2:def 11;
L4: for r being FinSequence of NAT holds
( not r in dom t or not mu = xi ^ r or not F1 . mu = t . r ) by L3, TREES_1:1;
g /. b1 in dom Fi by I2;
then L6: ( xi in dom (Fi -sub (D . bi)) & g /. b1 in dom F1 ) by I2, L1;
then g /. b1 in (dom (Fi -sub (D . bi))) with-replacement (xi,(dom t)) by H7, F3, TREES_2:def 11;
hence (F . b) . (g /. b1) = [(V1 . b1),(B . b1)] by H2, L4, L6, L7, F3, H7, TREES_2:def 11; :: thesis:

end;

L8: for i being Nat st i >= 1 holds
S₁[i] from NAT_1:sch 8(F1, WW);
F is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y -context-sequence

proof

thus dom F = dom B by A7; :: according to MSAFREE5:def 38 :: thesis:
let b be Element of dom B; :: thesis:
1 <= b by FINSEQ_3:25;
hence F . b is context of the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b by L8; :: thesis:

end;

then reconsider F = F as the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y -context-sequence FinSequence of (Free (S,Y)) ;
take F ; :: thesis:
thus F is V1, the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y,D -consequent-context-sequence :: thesis:

proof

let i, j be Element of dom B; :: according to MSAFREE5:def 40 :: thesis:
reconsider nu = g /. i, xi = g /. j as Node of v ;
reconsider Fi = F . i, Fj = F . j as Element of (Free (S,Y)) ;
reconsider t = ( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . j) -term as Element of (Free (S,Y)) ;
H1: i >= 1 by FINSEQ_3:25;
assume H2: i + 1 = j ; :: thesis:
H3: j >= 1 by H2, NAT_1:12;
F3: F . j = (Fi with-replacement (nu,(D . i))) with-replacement (xi,t) by A7, H2;
H8: ( j > i & F /. i = Fi ) by A7, H2, NAT_1:13, PARTFUN1:def 6;
then H5: ( Fi is the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . j -omitting & Fi . xi = [(V1 . j),(B . j)] ) by H1, L8;
I2: ( D . i in the Sorts of (Free (S,Y)) . (B . i) & dom v c= dom Fi ) by H1, L8;
( nu = g . i & xi = g . j ) by AA, AB, PARTFUN1:def 6;
then H6: ( Fi . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . i),(B . i)] & the_sort_of (D . i) = B . i & nu in dom Fi & xi in dom Fi & nu <> xi ) by H1, AA, AB, I2, L8, H8, SORT, FUNCT_1:def 4;
then H7: Fi with-replacement (nu,(D . i)) = (F . i) -sub (D . i) by Th118;
reconsider q = (V1 . j) -term as Element of (Free (S,Y)) ;
M1: not nu c= xi by H6, Lem9;
then H4: for r being FinSequence of NAT holds
( not r in dom (D . i) or not xi = nu ^ r or not ((F . i) -sub (D . i)) . xi = (D . i) . r ) by TREES_1:1;
not nu c< xi by M1, XBOOLE_0:def 8;
then xi in (dom Fi) with-replacement (nu,(dom (D . i))) by H6, TREES_1:def 9;
then M8: ( ((F . i) -sub (D . i)) . xi = [(V1 . j),(B . j)] & xi in dom ((F . i) -sub (D . i)) ) by H4, H5, H6, H7, TREES_2:def 11;
then M3: ( dom ((F . i) -sub (D . i)) = dom Fj & dom v c= dom Fj ) by H3, L8, F3, H7, Lem11A;
M2: ( Fj . xi = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . j),(B . j)] & the_sort_of q = B . j & xi in dom Fj ) by M8, H3, L8, SORT, F3, H7, Lem11A;
then M5: (F . j) -sub q = (F . j) with-replacement (xi,q) by Th118;
hence M4: dom ((F . j) -sub ((V1 . j) -term)) = dom ((F . i) -sub (D . i)) by M3, M2, Lem11A; :: according to TREES_4:def 1 :: thesis:
let a be Node of ((F . j) -sub ((V1 . j) -term)); :: thesis:
( a in dom ((F . j) -sub ((V1 . j) -term)) & dom ((F . j) -sub ((V1 . j) -term)) = (dom Fj) with-replacement (xi,(dom q)) ) by M2, M5, TREES_2:def 11;

per cases by M5, M2, TREES_2:def 11;

suppose M6: ( not xi c= a & ((F . j) -sub q) . a = Fj . a ) ; :: thesis:

then not xi c< a by XBOOLE_0:def 8;
then M7: a in (dom ((F . i) -sub (D . i))) with-replacement (xi,(dom t)) by M8, M4, TREES_1:def 9;
for r being FinSequence of NAT holds
( not r in dom t or not a = xi ^ r or not Fj . a = t . r ) by M6, TREES_1:1;
hence ((F . j) -sub ((V1 . j) -term)) . a = ((F . i) -sub (D . i)) . a by F3, H7, M6, M7, M8, TREES_2:def 11; :: thesis:

end;

suppose ex r being FinSequence of NAT st
( r in dom q & a = xi ^ r & ((F . j) -sub q) . a = q . r ) ; :: thesis:

then consider r being FinSequence of NAT such that
N1: ( r in dom q & a = xi ^ r & ((F . j) -sub q) . a = q . r ) ;
r in {{}} by N1, TREES_1:29;
then r = {} ;
hence ((F . j) -sub ((V1 . j) -term)) . a = ((F . i) -sub (D . i)) . a by M8, N1, TREES_4:3; :: thesis:

end;

set b = In (1,(dom B));
reconsider nu = g /. (In (1,(dom B))), xi = g /. (len B) as Node of v ;
NK: ( 1 <= In (1,(dom B)) & In (1,(dom B)) <= len B ) by FINSEQ_3:25;
N6: F . (In (1,(dom B))) = v with-replacement (nu,(( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term)) by A7;
NM: nu = g . (In (1,(dom B))) by AA, AB, PARTFUN1:def 6;
then ( v . nu = f . (In (1,(dom B))) & nu in rng g ) by AB, AA, FUNCT_1:def 3;
then consider mu being Node of v such that
N5: ( nu = mu & ex s being SortSymbol of S ex y being Element of Y . s st v . mu = [y,s] ) by AA;
reconsider fb = f . (In (1,(dom B))) as pair object by NM, N5, AB, AA;
N7: v . nu = [(fb `1),(fb `2)] by NM, AB, AA
.= [(V1 . (In (1,(dom B)))),(fb `2)] by AB, MCART_1:def 12
.= [(V1 . (In (1,(dom B)))),(B . (In (1,(dom B))))] by AB, MCART_1:def 13 ;
then N8: dom (F . (In (1,(dom B)))) = dom v by N6, Lem11A;
reconsider t = (V1 . (In (1,(dom B)))) -term as Element of (Free (S,Y)) ;
O3: dom (F . (In (1,(dom B)))) = (dom v) with-replacement (nu,(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term))) by A7, TREES_2:def 11;
then consider mu being FinSequence of NAT such that
N9: ( mu in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) & nu = nu ^ mu & (F . (In (1,(dom B)))) . nu = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) . mu ) by A7, N8, TREES_2:def 11;
OA: mu = {} by N9, FINSEQ_1:87;
then ( (F . (In (1,(dom B)))) . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))),(B . (In (1,(dom B))))] & the_sort_of t = B . (In (1,(dom B))) ) by N9, SORT, TREES_4:3;
then O1: (F . (In (1,(dom B)))) -sub t = (F . (In (1,(dom B)))) with-replacement (nu,t) by N8, Th118;
hence O5: dom ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) = dom v by N8, OA, Lem11A, N9, TREES_4:3; :: according to TREES_4:def 1 :: thesis:

hereby :: thesis:

let a be Node of ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)); :: thesis:
dom ((F . (In (1,(dom B)))) -sub t) = (dom (F . (In (1,(dom B))))) with-replacement (nu,(dom t)) by N8, O1, TREES_2:def 11;

per cases by N8, O1, TREES_2:def 11;

suppose O4: ( not nu c= a & ((F . (In (1,(dom B)))) -sub t) . a = (F . (In (1,(dom B)))) . a ) ; :: thesis:

then for r being FinSequence of NAT holds
( not r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) or not a = nu ^ r or not (F . (In (1,(dom B)))) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In (1,(dom B)))) -term) . r ) by TREES_1:1;
hence ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) . a = v . a by A7, N8, O3, O4, O5, TREES_2:def 11; :: thesis:

end;

suppose ex r being FinSequence of NAT st
( r in dom t & a = nu ^ r & ((F . (In (1,(dom B)))) -sub t) . a = t . r ) ; :: thesis:

then consider r being FinSequence of NAT such that
O6: ( r in dom t & a = nu ^ r & ((F . (In (1,(dom B)))) -sub t) . a = t . r ) ;
r in {{}} by O6, TREES_1:29;
then r = {} ;
hence ((F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term)) . a = v . a by N7, O6, TREES_4:3; :: thesis:

end;

defpred S₂[ Nat] means for b, b1 being Element of dom B st $1 = b & b1 <= b holds
( ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) & ((F . b) -sub (D . b)) | ((dom v) \ (rng g)) = v | ((dom v) \ (rng g)) );
S1: S₂[1]

proof

let b, b1 be Element of dom B; :: thesis:
assume S2: ( 1 = b & b1 <= b ) ; :: thesis:
b1 >= 1 by FINSEQ_3:25;
then S3: b1 = 1 by S2, XXREAL_0:1;
reconsider nu = g /. b as Node of v ;
S4: ( (F . b) . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & nu in dom v & dom v c= dom (F . b) & the_sort_of (D . b) = B . b ) by S2, F1, SORT;
then S8: (F . b) -sub (D . b) = (F . b) with-replacement (nu,(D . b)) by Th118;
then S7: ((F . b) -sub (D . b)) | nu = D . b by S4, Th130;
SD: nu = g . b by AA, AB, PARTFUN1:def 6;
then S5: ( v . nu = f . b & nu in rng g ) by AA, AB, FUNCT_1:def 3;
then consider mu being Node of v such that
S6: ( nu = mu & ex s being SortSymbol of S ex y being Element of Y . s st v . mu = [y,s] ) by AA;
reconsider fb = f . b as pair object by SD, S6, AA, AB;
SC: v . nu = [(fb `1),(fb `2)] by SD, AA, AB
.= [(V1 . b),(fb `2)] by AB, MCART_1:def 12
.= [(V1 . b),(B . b)] by AB, MCART_1:def 13 ;
then v | nu = (V1 . b) -term by Th132;
then (h . v) | nu = h . ((V1 . b) -term) by Th131;
hence ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) by A2, S7, S2, S3; :: thesis:
dom (F . b) c= dom ((F . b) -sub (D . b)) by S4, S8, Lem11;
then (dom v) \ (rng g) c= dom ((F . b) -sub (D . b)) by S4;
hence dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) = dom (v | ((dom v) \ (rng g))) by RELAT_1:62; :: according to FUNCT_1:def 11 :: thesis:
let a be object ; :: thesis:
assume SK: a in dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) ; :: thesis:
then a in (dom v) \ (rng g) ;
then reconsider a = a as Node of v ;
SJ: ( (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = ((F . b) -sub (D . b)) . a & (v | ((dom v) \ (rng g))) . a = v . a ) by SK, FUNCT_1:49;
nu <> a by S5, SK, XBOOLE_0:def 5;
then SD: not nu c= a by SC, Lem9;
then SE: for r being FinSequence of NAT holds
( not r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not a = nu ^ r or not (F . b) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r ) by TREES_1:1;
SG: not nu c< a by SD, XBOOLE_0:def 8;
then a in (dom v) with-replacement (nu,(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) by TREES_1:def 9;
then SI: v . a = (F . b) . a by A7, S2, SE, TREES_2:def 11;
SF: for r being FinSequence of NAT holds
( not r in dom (D . b) or not a = nu ^ r or not ((F . b) -sub (D . b)) . a = (D . b) . r ) by SD, TREES_1:1;
( a in dom (F . b) & nu in dom (F . b) ) by S4;
then a in (dom (F . b)) with-replacement (nu,(dom (D . b))) by SG, TREES_1:def 9;
hence (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a by SI, SJ, SF, S4, S8, TREES_2:def 11; :: thesis:

end;

T1: for i being Nat st i >= 1 & S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume T2: ( i >= 1 & S₂[i] ) ; :: thesis:
let b, b1 be Element of dom B; :: thesis:
assume T3: ( b = i + 1 & b1 <= b ) ; :: thesis:
then i + 1 <= len B by FINSEQ_3:25;
then i < len B by NAT_1:13;
then reconsider b2 = i as Element of dom B by T2, FINSEQ_3:25;
T5: F . b = ((F . b2) with-replacement ((g /. b2),(D . b2))) with-replacement ((g /. b),(( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term)) by A7, T3;
( v . (g . b) = f . b & g . b in rng g ) by AA, AB, FUNCT_1:def 3;
then consider nu being Node of v such that
U2: ( g . b = nu & ex s being SortSymbol of S ex y being Element of Y . s st v . nu = [y,s] ) by AA;
reconsider fb = f . b as pair object by U2, AA, AB;
U3: v . (g /. b) = v . (g . b) by AA, AB, PARTFUN1:def 6
.= [(fb `1),(fb `2)] by AA, AB
.= [(V1 . b),(fb `2)] by AB, MCART_1:def 12
.= [(V1 . b),(B . b)] by AB, MCART_1:def 13 ;
T7: ( the_sort_of (D . b2) = B . b2 & (F . b2) . (g /. b2) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b2),(B . b2)] & g /. b2 in dom v & dom v c= dom (F . b2) ) by T2, L8, SORT;
then T6: (F . b2) -sub (D . b2) = (F . b2) with-replacement ((g /. b2),(D . b2)) by Th118;
T18: ( g /. b1 = g . b1 & g /. b = g . b ) by AA, AB, PARTFUN1:def 6;
dom (F . b2) c= dom ((F . b2) -sub (D . b2)) by T6, T7, Lem11;
then T21: ( g /. b in dom ((F . b2) -sub (D . b2)) & g /. b1 in dom ((F . b2) -sub (D . b2)) ) by T7;

per cases by T3, XXREAL_0:1;

suppose b1 < b ; :: thesis:

then T8: ( b1 <= b2 & g . b1 <> g . b ) by AA, AB, T3, FUNCT_1:def 4, NAT_1:13;
then T4: ((F . b2) -sub (D . b2)) | (g /. b1) = (h . v) | (g /. b1) by T2;
( v . (g . b1) = f . b1 & g . b1 in rng g ) by AA, AB, FUNCT_1:def 3;
then consider nu being Node of v such that
U5: ( g . b1 = nu & ex s being SortSymbol of S ex y being Element of Y . s st v . nu = [y,s] ) by AA;
reconsider fb1 = f . b1 as pair object by U5, AA, AB;
U6: v . (g /. b1) = v . (g . b1) by AA, AB, PARTFUN1:def 6
.= [(fb1 `1),(fb1 `2)] by AA, AB
.= [(V1 . b1),(fb1 `2)] by AB, MCART_1:def 12
.= [(V1 . b1),(B . b1)] by AB, MCART_1:def 13 ;
T9: ( not g /. b c= g /. b1 & not g /. b1 c= g /. b ) by T18, T8, U3, U6, Lem9;
then T10: (F . b) | (g /. b1) = (h . v) | (g /. b1) by T21, T4, T5, T6, Th133;
1 <= i + 1 by NAT_1:12;
then T12: ( (F . b) . (g /. b) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & g /. b in dom v & dom v c= dom (F . b) & g /. b1 in dom v & the_sort_of (D . b) = B . b ) by T3, L8, SORT;
then T11: (F . b) -sub (D . b) = (F . b) with-replacement ((g /. b),(D . b)) by Th118;
hence ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) by T10, T12, T9, Th133; :: thesis:
( dom v c= dom (F . b) & dom (F . b) c= dom ((F . b) -sub (D . b)) ) by T12, T11, Lem11;
then (dom v) \ (rng g) c= dom ((F . b) -sub (D . b)) ;
hence dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) = dom (v | ((dom v) \ (rng g))) by RELAT_1:62; :: according to FUNCT_1:def 11 :: thesis:
let a be object ; :: thesis:
assume TT: a in dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) ; :: thesis:
reconsider a = a as Node of ((F . b) -sub (D . b)) by TT, RELAT_1:57;
T16: ( (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = ((F . b) -sub (D . b)) . a & (((F . b2) -sub (D . b2)) | ((dom v) \ (rng g))) . a = ((F . b2) -sub (D . b2)) . a & (v | ((dom v) \ (rng g))) . a = v . a ) by TT, FUNCT_1:49;
then T17: ((F . b2) -sub (D . b2)) . a = v . a by T2;
( g /. b in rng g & a nin rng g & a in dom v ) by T18, AA, AB, TT, XBOOLE_0:def 5, FUNCT_1:def 3;
then T19: ( not g /. b c= a & a in dom (F . b) & dom (F . b) = (dom ((F . b2) -sub (D . b2))) with-replacement ((g /. b),(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) ) by T18, U2, T21, T5, T6, T12, Lem9, TREES_2:def 11;
then for r being FinSequence of NAT holds
( not r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not a = (g /. b) ^ r or not (F . b) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r ) by TREES_1:1;
then T22: (F . b) . a = v . a by T18, U2, T17, T19, T21, T5, T6, TREES_2:def 11;
T24: ( a in dom ((F . b) -sub (D . b)) & dom ((F . b) -sub (D . b)) = (dom (F . b)) with-replacement ((g /. b),(dom (D . b))) ) by T12, T18, U2, T11, TREES_2:def 11;
for r being FinSequence of NAT holds
( not r in dom (D . b) or not a = (g /. b) ^ r or not ((F . b) -sub (D . b)) . a = (D . b) . r ) by T19, TREES_1:1;
hence (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a by T16, T18, U2, T11, T22, T12, T24, TREES_2:def 11; :: thesis:

end;

suppose U7: b1 = b ; :: thesis:

reconsider nu = g /. b as Node of v ;
i + 1 >= 1 by NAT_1:12;
then S4: ( (F . b) . nu = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b),(B . b)] & nu in dom v & dom v c= dom (F . b) & the_sort_of (D . b) = B . b ) by T3, L8, SORT;
then T11: (F . b) -sub (D . b) = (F . b) with-replacement (nu,(D . b)) by Th118;
then S7: ((F . b) -sub (D . b)) | nu = D . b by S4, Th130;
T18: nu = g . b by AA, AB, PARTFUN1:def 6;
then ( v . nu = f . b & nu in rng g ) by AA, AB, FUNCT_1:def 3;
then consider mu being Node of v such that
S6: ( nu = mu & ex s being SortSymbol of S ex y being Element of Y . s st v . mu = [y,s] ) by AA;
reconsider fb = f . b as pair object by T18, S6, AA, AB;
v . nu = [(fb `1),(fb `2)] by T18, AA, AB
.= [(V1 . b),(fb `2)] by AB, MCART_1:def 12
.= [(V1 . b),(B . b)] by AB, MCART_1:def 13 ;
then v | nu = (V1 . b) -term by Th132;
then (h . v) | nu = h . ((V1 . b) -term) by Th131;
hence ((F . b) -sub (D . b)) | (g /. b1) = (h . v) | (g /. b1) by A2, S7, U7; :: thesis:
( dom v c= dom (F . b) & dom (F . b) c= dom ((F . b) -sub (D . b)) ) by S4, T11, Lem11;
then (dom v) \ (rng g) c= dom ((F . b) -sub (D . b)) ;
hence dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) = dom (v | ((dom v) \ (rng g))) by RELAT_1:62; :: according to FUNCT_1:def 11 :: thesis:
let a be object ; :: thesis:
assume T24: a in dom (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) ; :: thesis:
then reconsider a = a as Node of ((F . b) -sub (D . b)) by RELAT_1:57;
T16: ( (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = ((F . b) -sub (D . b)) . a & (((F . b2) -sub (D . b2)) | ((dom v) \ (rng g))) . a = ((F . b2) -sub (D . b2)) . a & (v | ((dom v) \ (rng g))) . a = v . a ) by T24, FUNCT_1:49;
then T17: ((F . b2) -sub (D . b2)) . a = v . a by T2;
( g /. b in rng g & a nin rng g & a in dom v ) by T18, AA, AB, T24, XBOOLE_0:def 5, FUNCT_1:def 3;
then T19: ( not g /. b c= a & a in dom (F . b) & dom (F . b) = (dom ((F . b2) -sub (D . b2))) with-replacement ((g /. b),(dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term))) ) by T21, T5, T6, S4, Lem9, TREES_2:def 11;
then for r being FinSequence of NAT holds
( not r in dom (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) or not a = (g /. b) ^ r or not (F . b) . a = (( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . b) -term) . r ) by TREES_1:1;
then T22: (F . b) . a = v . a by T18, T17, T19, T21, T5, T6, TREES_2:def 11;
T24: ( a in dom ((F . b) -sub (D . b)) & dom ((F . b) -sub (D . b)) = (dom (F . b)) with-replacement ((g /. b),(dom (D . b))) ) by S4, T11, TREES_2:def 11;
for r being FinSequence of NAT holds
( not r in dom (D . b) or not a = (g /. b) ^ r or not ((F . b) -sub (D . b)) . a = (D . b) . r ) by T19, TREES_1:1;
hence (((F . b) -sub (D . b)) | ((dom v) \ (rng g))) . a = (v | ((dom v) \ (rng g))) . a by T16, T11, T22, S4, T24, TREES_2:def 11; :: thesis:

end;

set b = In ((len B),(dom B));
set v1 = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))));
SK: for i being Nat st i >= 1 holds
S₂[i] from NAT_1:sch 8(S1, T1);
S8: ( (F . (In ((len B),(dom B)))) . (g /. (In ((len B),(dom B)))) = [( the one-to-one B -sorts V1 -omitting D -omitting FinSequence of Union Y . (In ((len B),(dom B)))),(B . (In ((len B),(dom B))))] & dom v c= dom (F . (In ((len B),(dom B)))) ) by L8, NK;
then SA: ( the_sort_of (D . (In ((len B),(dom B)))) = B . (In ((len B),(dom B))) & g /. (In ((len B),(dom B))) in dom (F . (In ((len B),(dom B)))) ) by SORT;
then (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) = (F . (In ((len B),(dom B)))) with-replacement ((g /. (In ((len B),(dom B)))),(D . (In ((len B),(dom B))))) by S8, Th118;
then dom (F . (In ((len B),(dom B)))) c= dom ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))) by SA, S8, Lem11;
then S9: ( dom v c= dom ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))) & v | ((dom v) \ (rng g)) = ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))) | ((dom v) \ (rng g)) ) by SK, S8, NK;

now :: thesis:

let i be Nat; :: thesis:
assume i in dom g ; :: thesis:
then reconsider b1 = i as Element of dom B by AA, MCART_1:def 13;
b1 <= len B by FINSEQ_3:25;
hence (h . v) | (g /. i) = ((F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B))))) | (g /. i) by SK, NK; :: thesis:

end;

hence h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) by AA, S9, Th138; :: thesis: