let T1, T2 be DecoratedTree of NAT ; :: thesis: ( T1 . {} = FirstLoc M & ( for t being Element of dom T1 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds

T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) ) & T2 . {} = FirstLoc M & ( for t being Element of dom T2 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds

T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ) implies T1 = T2 )

assume that

A13: T1 . {} = FirstLoc M and

A14: for t being Element of dom T1 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds

T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) and

A15: T2 . {} = FirstLoc M and

A16: for t being Element of dom T2 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds

T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ; :: thesis: T1 = T2

defpred S_{1}[ Nat] means (dom T1) -level $1 = (dom T2) -level $1;

A17: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= (dom T2) -level 0 by TREES_9:44 ;

then A74: S_{1}[ 0 ]
;

A75: for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A74, A17);

for p being FinSequence of NAT st p in dom T1 holds

T1 . p = T2 . p

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds

T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) ) & T2 . {} = FirstLoc M & ( for t being Element of dom T2 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds

T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ) implies T1 = T2 )

assume that

A13: T1 . {} = FirstLoc M and

A14: for t being Element of dom T1 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t)),(T1 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T1 . t)),(T1 . t))) holds

T1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T1 . t)),(T1 . t))),S)) . m ) ) and

A15: T2 . {} = FirstLoc M and

A16: for t being Element of dom T2 holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . t)),(T2 . t))) } & ( for m being Nat st m in card (NIC ((M /. (T2 . t)),(T2 . t))) holds

T2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T2 . t)),(T2 . t))),S)) . m ) ) ; :: thesis: T1 = T2

defpred S

A17: for n being Nat st S

S

proof

(dom T1) -level 0 =
{{}}
by TREES_9:44
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A18: S_{1}[n]
; :: thesis: S_{1}[n + 1]

set U2 = { (succ w) where w is Element of dom T2 : len w = n } ;

set U1 = { (succ w) where w is Element of dom T1 : len w = n } ;

A19: (dom T2) -level n = { v where v is Element of dom T2 : len v = n } by TREES_2:def 6;

A20: (dom T1) -level n = { v where v is Element of dom T1 : len v = n } by TREES_2:def 6;

A21: union { (succ w) where w is Element of dom T1 : len w = n } = union { (succ w) where w is Element of dom T2 : len w = n }

hence S_{1}[n + 1]
by A21, TREES_9:45; :: thesis: verum

end;assume A18: S

set U2 = { (succ w) where w is Element of dom T2 : len w = n } ;

set U1 = { (succ w) where w is Element of dom T1 : len w = n } ;

A19: (dom T2) -level n = { v where v is Element of dom T2 : len v = n } by TREES_2:def 6;

A20: (dom T1) -level n = { v where v is Element of dom T1 : len v = n } by TREES_2:def 6;

A21: union { (succ w) where w is Element of dom T1 : len w = n } = union { (succ w) where w is Element of dom T2 : len w = n }

proof

assume a in union { (succ w) where w is Element of dom T2 : len w = n } ; :: thesis: a in union { (succ w) where w is Element of dom T1 : len w = n }

then consider A being set such that

A48: a in A and

A49: A in { (succ w) where w is Element of dom T2 : len w = n } by TARSKI:def 4;

consider w being Element of dom T2 such that

A50: A = succ w and

A51: len w = n by A49;

w in (dom T2) -level n by A19, A51;

then consider v being Element of dom T1 such that

A52: w = v and

A53: len v = n by A18, A20;

A54: w = w | (Seg (len w)) by FINSEQ_3:49;

defpred S_{2}[ Nat] means ( $1 <= len w & w | (Seg $1) in dom T1 & v | (Seg $1) in dom T2 implies T1 . (w | (Seg $1)) = T2 . (w | (Seg $1)) );

A55: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
by A13, A15;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A71, A55);

then A72: T1 . w = T2 . w by A52, A54;

A73: succ v in { (succ w) where w is Element of dom T1 : len w = n } by A53;

( succ v = { (v ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . v)),(T1 . v))) } & succ w = { (w ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . w)),(T2 . w))) } ) by A14, A16;

hence a in union { (succ w) where w is Element of dom T1 : len w = n } by A48, A50, A52, A72, A73, TARSKI:def 4; :: thesis: verum

end;

(dom T1) -level (n + 1) = union { (succ w) where w is Element of dom T1 : len w = n }
by TREES_9:45;hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (succ w) where w is Element of dom T2 : len w = n } c= union { (succ w) where w is Element of dom T1 : len w = n }

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (succ w) where w is Element of dom T2 : len w = n } or a in union { (succ w) where w is Element of dom T1 : len w = n } )let a be object ; :: thesis: ( a in union { (succ w) where w is Element of dom T1 : len w = n } implies a in union { (succ w) where w is Element of dom T2 : len w = n } )

assume a in union { (succ w) where w is Element of dom T1 : len w = n } ; :: thesis: a in union { (succ w) where w is Element of dom T2 : len w = n }

then consider A being set such that

A22: a in A and

A23: A in { (succ w) where w is Element of dom T1 : len w = n } by TARSKI:def 4;

consider w being Element of dom T1 such that

A24: A = succ w and

A25: len w = n by A23;

w in (dom T1) -level n by A20, A25;

then consider v being Element of dom T2 such that

A26: w = v and

A27: len v = n by A18, A19;

A28: w = w | (Seg (len w)) by FINSEQ_3:49;

defpred S_{2}[ Nat] means ( $1 <= len w & w | (Seg $1) in dom T1 & v | (Seg $1) in dom T2 implies T1 . (w | (Seg $1)) = T2 . (w | (Seg $1)) );

A29: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
by A13, A15;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A45, A29);

then A46: T1 . w = T2 . w by A26, A28;

A47: succ v in { (succ w) where w is Element of dom T2 : len w = n } by A27;

( succ v = { (v ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . v)),(T2 . v))) } & succ w = { (w ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . w)),(T1 . w))) } ) by A14, A16;

hence a in union { (succ w) where w is Element of dom T2 : len w = n } by A22, A24, A26, A46, A47, TARSKI:def 4; :: thesis: verum

end;assume a in union { (succ w) where w is Element of dom T1 : len w = n } ; :: thesis: a in union { (succ w) where w is Element of dom T2 : len w = n }

then consider A being set such that

A22: a in A and

A23: A in { (succ w) where w is Element of dom T1 : len w = n } by TARSKI:def 4;

consider w being Element of dom T1 such that

A24: A = succ w and

A25: len w = n by A23;

w in (dom T1) -level n by A20, A25;

then consider v being Element of dom T2 such that

A26: w = v and

A27: len v = n by A18, A19;

A28: w = w | (Seg (len w)) by FINSEQ_3:49;

defpred S

A29: for n being Nat st S

S

proof

A45:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume that

A30: S_{2}[n]
and

A31: n + 1 <= len w and

A32: w | (Seg (n + 1)) in dom T1 and

A33: v | (Seg (n + 1)) in dom T2 ; :: thesis: T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))

set t1 = w | (Seg n);

A34: 1 <= n + 1 by NAT_1:11;

A35: len (w | (Seg (n + 1))) = n + 1 by A31, FINSEQ_1:17;

then len (w | (Seg (n + 1))) in Seg (n + 1) by A34, FINSEQ_1:1;

then A36: w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A35, FUNCT_1:49;

n + 1 in dom w by A31, A34, FINSEQ_3:25;

then A37: w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> by A36, FINSEQ_5:10;

A38: n <= n + 1 by NAT_1:11;

then A39: Seg n c= Seg (n + 1) by FINSEQ_1:5;

then v | (Seg n) = (v | (Seg (n + 1))) | (Seg n) by RELAT_1:74;

then A40: v | (Seg n) is_a_prefix_of v | (Seg (n + 1)) by TREES_1:def 1;

w | (Seg n) = (w | (Seg (n + 1))) | (Seg n) by A39, RELAT_1:74;

then w | (Seg n) is_a_prefix_of w | (Seg (n + 1)) by TREES_1:def 1;

then reconsider t1 = w | (Seg n) as Element of dom T1 by A32, TREES_1:20;

reconsider t2 = t1 as Element of dom T2 by A26, A33, A40, TREES_1:20;

A41: succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A14;

t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1 by A32, A37, TREES_2:12;

then consider k being Nat such that

A42: t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*> and

A43: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A41;

A44: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A30, A31, A33, A38, A40, A42, A43, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;

k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A42, FINSEQ_2:17;

hence T1 . (w | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))) by A14, A37, A43

.= T2 . (w | (Seg (n + 1))) by A16, A30, A31, A33, A38, A40, A37, A44, TREES_1:20, XXREAL_0:2 ;

:: thesis: verum

end;assume that

A30: S

A31: n + 1 <= len w and

A32: w | (Seg (n + 1)) in dom T1 and

A33: v | (Seg (n + 1)) in dom T2 ; :: thesis: T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))

set t1 = w | (Seg n);

A34: 1 <= n + 1 by NAT_1:11;

A35: len (w | (Seg (n + 1))) = n + 1 by A31, FINSEQ_1:17;

then len (w | (Seg (n + 1))) in Seg (n + 1) by A34, FINSEQ_1:1;

then A36: w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A35, FUNCT_1:49;

n + 1 in dom w by A31, A34, FINSEQ_3:25;

then A37: w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> by A36, FINSEQ_5:10;

A38: n <= n + 1 by NAT_1:11;

then A39: Seg n c= Seg (n + 1) by FINSEQ_1:5;

then v | (Seg n) = (v | (Seg (n + 1))) | (Seg n) by RELAT_1:74;

then A40: v | (Seg n) is_a_prefix_of v | (Seg (n + 1)) by TREES_1:def 1;

w | (Seg n) = (w | (Seg (n + 1))) | (Seg n) by A39, RELAT_1:74;

then w | (Seg n) is_a_prefix_of w | (Seg (n + 1)) by TREES_1:def 1;

then reconsider t1 = w | (Seg n) as Element of dom T1 by A32, TREES_1:20;

reconsider t2 = t1 as Element of dom T2 by A26, A33, A40, TREES_1:20;

A41: succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A14;

t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1 by A32, A37, TREES_2:12;

then consider k being Nat such that

A42: t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*> and

A43: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A41;

A44: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A30, A31, A33, A38, A40, A42, A43, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;

k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A42, FINSEQ_2:17;

hence T1 . (w | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))) by A14, A37, A43

.= T2 . (w | (Seg (n + 1))) by A16, A30, A31, A33, A38, A40, A37, A44, TREES_1:20, XXREAL_0:2 ;

:: thesis: verum

for n being Nat holds S

then A46: T1 . w = T2 . w by A26, A28;

A47: succ v in { (succ w) where w is Element of dom T2 : len w = n } by A27;

( succ v = { (v ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . v)),(T2 . v))) } & succ w = { (w ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . w)),(T1 . w))) } ) by A14, A16;

hence a in union { (succ w) where w is Element of dom T2 : len w = n } by A22, A24, A26, A46, A47, TARSKI:def 4; :: thesis: verum

assume a in union { (succ w) where w is Element of dom T2 : len w = n } ; :: thesis: a in union { (succ w) where w is Element of dom T1 : len w = n }

then consider A being set such that

A48: a in A and

A49: A in { (succ w) where w is Element of dom T2 : len w = n } by TARSKI:def 4;

consider w being Element of dom T2 such that

A50: A = succ w and

A51: len w = n by A49;

w in (dom T2) -level n by A19, A51;

then consider v being Element of dom T1 such that

A52: w = v and

A53: len v = n by A18, A20;

A54: w = w | (Seg (len w)) by FINSEQ_3:49;

defpred S

A55: for n being Nat st S

S

proof

A71:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume that

A56: S_{2}[n]
and

A57: n + 1 <= len w and

A58: w | (Seg (n + 1)) in dom T1 and

A59: v | (Seg (n + 1)) in dom T2 ; :: thesis: T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))

set t1 = w | (Seg n);

A60: 1 <= n + 1 by NAT_1:11;

A61: len (w | (Seg (n + 1))) = n + 1 by A57, FINSEQ_1:17;

then len (w | (Seg (n + 1))) in Seg (n + 1) by A60, FINSEQ_1:1;

then A62: w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A61, FUNCT_1:49;

n + 1 in dom w by A57, A60, FINSEQ_3:25;

then A63: w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> by A62, FINSEQ_5:10;

A64: n <= n + 1 by NAT_1:11;

then A65: Seg n c= Seg (n + 1) by FINSEQ_1:5;

then v | (Seg n) = (v | (Seg (n + 1))) | (Seg n) by RELAT_1:74;

then A66: v | (Seg n) is_a_prefix_of v | (Seg (n + 1)) by TREES_1:def 1;

w | (Seg n) = (w | (Seg (n + 1))) | (Seg n) by A65, RELAT_1:74;

then w | (Seg n) is_a_prefix_of w | (Seg (n + 1)) by TREES_1:def 1;

then reconsider t1 = w | (Seg n) as Element of dom T1 by A58, TREES_1:20;

reconsider t2 = t1 as Element of dom T2 by A52, A59, A66, TREES_1:20;

A67: succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A14;

t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1 by A58, A63, TREES_2:12;

then consider k being Nat such that

A68: t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*> and

A69: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A67;

A70: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A56, A57, A59, A64, A66, A68, A69, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;

k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A68, FINSEQ_2:17;

hence T1 . (w | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))) by A14, A63, A69

.= T2 . (w | (Seg (n + 1))) by A16, A56, A57, A59, A64, A66, A63, A70, TREES_1:20, XXREAL_0:2 ;

:: thesis: verum

end;assume that

A56: S

A57: n + 1 <= len w and

A58: w | (Seg (n + 1)) in dom T1 and

A59: v | (Seg (n + 1)) in dom T2 ; :: thesis: T1 . (w | (Seg (n + 1))) = T2 . (w | (Seg (n + 1)))

set t1 = w | (Seg n);

A60: 1 <= n + 1 by NAT_1:11;

A61: len (w | (Seg (n + 1))) = n + 1 by A57, FINSEQ_1:17;

then len (w | (Seg (n + 1))) in Seg (n + 1) by A60, FINSEQ_1:1;

then A62: w . (n + 1) = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A61, FUNCT_1:49;

n + 1 in dom w by A57, A60, FINSEQ_3:25;

then A63: w | (Seg (n + 1)) = (w | (Seg n)) ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> by A62, FINSEQ_5:10;

A64: n <= n + 1 by NAT_1:11;

then A65: Seg n c= Seg (n + 1) by FINSEQ_1:5;

then v | (Seg n) = (v | (Seg (n + 1))) | (Seg n) by RELAT_1:74;

then A66: v | (Seg n) is_a_prefix_of v | (Seg (n + 1)) by TREES_1:def 1;

w | (Seg n) = (w | (Seg (n + 1))) | (Seg n) by A65, RELAT_1:74;

then w | (Seg n) is_a_prefix_of w | (Seg (n + 1)) by TREES_1:def 1;

then reconsider t1 = w | (Seg n) as Element of dom T1 by A58, TREES_1:20;

reconsider t2 = t1 as Element of dom T2 by A52, A59, A66, TREES_1:20;

A67: succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A14;

t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> in succ t1 by A58, A63, TREES_2:12;

then consider k being Nat such that

A68: t1 ^ <*((w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))))*> = t1 ^ <*k*> and

A69: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A67;

A70: (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A56, A57, A59, A64, A66, A68, A69, FINSEQ_2:17, TREES_1:20, XXREAL_0:2;

k = (w | (Seg (n + 1))) . (len (w | (Seg (n + 1)))) by A68, FINSEQ_2:17;

hence T1 . (w | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | (Seg (n + 1))) . (len (w | (Seg (n + 1))))) by A14, A63, A69

.= T2 . (w | (Seg (n + 1))) by A16, A56, A57, A59, A64, A66, A63, A70, TREES_1:20, XXREAL_0:2 ;

:: thesis: verum

for n being Nat holds S

then A72: T1 . w = T2 . w by A52, A54;

A73: succ v in { (succ w) where w is Element of dom T1 : len w = n } by A53;

( succ v = { (v ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . v)),(T1 . v))) } & succ w = { (w ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T2 . w)),(T2 . w))) } ) by A14, A16;

hence a in union { (succ w) where w is Element of dom T1 : len w = n } by A48, A50, A52, A72, A73, TARSKI:def 4; :: thesis: verum

hence S

.= (dom T2) -level 0 by TREES_9:44 ;

then A74: S

A75: for n being Nat holds S

for p being FinSequence of NAT st p in dom T1 holds

T1 . p = T2 . p

proof

hence
T1 = T2
by A75, TREES_2:31, TREES_2:38; :: thesis: verum
let p be FinSequence of NAT ; :: thesis: ( p in dom T1 implies T1 . p = T2 . p )

defpred S_{2}[ Nat] means ( $1 <= len p & p | (Seg $1) in dom T1 implies T1 . (p | (Seg $1)) = T2 . (p | (Seg $1)) );

A76: p | (Seg (len p)) = p by FINSEQ_3:49;

A77: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
by A13, A15;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A90, A77);

hence ( p in dom T1 implies T1 . p = T2 . p ) by A76; :: thesis: verum

end;defpred S

A76: p | (Seg (len p)) = p by FINSEQ_3:49;

A77: for n being Nat st S

S

proof

A90:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume that

A78: S_{2}[n]
and

A79: n + 1 <= len p and

A80: p | (Seg (n + 1)) in dom T1 ; :: thesis: T1 . (p | (Seg (n + 1))) = T2 . (p | (Seg (n + 1)))

set t1 = p | (Seg n);

A81: 1 <= n + 1 by NAT_1:11;

A82: len (p | (Seg (n + 1))) = n + 1 by A79, FINSEQ_1:17;

then len (p | (Seg (n + 1))) in Seg (n + 1) by A81, FINSEQ_1:1;

then A83: p . (n + 1) = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) by A82, FUNCT_1:49;

n + 1 in dom p by A79, A81, FINSEQ_3:25;

then A84: p | (Seg (n + 1)) = (p | (Seg n)) ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> by A83, FINSEQ_5:10;

A85: n <= n + 1 by NAT_1:11;

then Seg n c= Seg (n + 1) by FINSEQ_1:5;

then p | (Seg n) = (p | (Seg (n + 1))) | (Seg n) by RELAT_1:74;

then p | (Seg n) is_a_prefix_of p | (Seg (n + 1)) by TREES_1:def 1;

then reconsider t1 = p | (Seg n) as Element of dom T1 by A80, TREES_1:20;

reconsider t2 = t1 as Element of dom T2 by A75, TREES_2:38;

A86: succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A14;

t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> in succ t1 by A80, A84, TREES_2:12;

then consider k being Nat such that

A87: t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> = t1 ^ <*k*> and

A88: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A86;

A89: (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A78, A79, A85, A87, A88, FINSEQ_2:17, XXREAL_0:2;

k = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) by A87, FINSEQ_2:17;

hence T1 . (p | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))) by A14, A84, A88

.= T2 . (p | (Seg (n + 1))) by A16, A78, A79, A85, A84, A89, XXREAL_0:2 ;

:: thesis: verum

end;assume that

A78: S

A79: n + 1 <= len p and

A80: p | (Seg (n + 1)) in dom T1 ; :: thesis: T1 . (p | (Seg (n + 1))) = T2 . (p | (Seg (n + 1)))

set t1 = p | (Seg n);

A81: 1 <= n + 1 by NAT_1:11;

A82: len (p | (Seg (n + 1))) = n + 1 by A79, FINSEQ_1:17;

then len (p | (Seg (n + 1))) in Seg (n + 1) by A81, FINSEQ_1:1;

then A83: p . (n + 1) = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) by A82, FUNCT_1:49;

n + 1 in dom p by A79, A81, FINSEQ_3:25;

then A84: p | (Seg (n + 1)) = (p | (Seg n)) ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> by A83, FINSEQ_5:10;

A85: n <= n + 1 by NAT_1:11;

then Seg n c= Seg (n + 1) by FINSEQ_1:5;

then p | (Seg n) = (p | (Seg (n + 1))) | (Seg n) by RELAT_1:74;

then p | (Seg n) is_a_prefix_of p | (Seg (n + 1)) by TREES_1:def 1;

then reconsider t1 = p | (Seg n) as Element of dom T1 by A80, TREES_1:20;

reconsider t2 = t1 as Element of dom T2 by A75, TREES_2:38;

A86: succ t1 = { (t1 ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) } by A14;

t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> in succ t1 by A80, A84, TREES_2:12;

then consider k being Nat such that

A87: t1 ^ <*((p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))))*> = t1 ^ <*k*> and

A88: k in card (NIC ((M /. (T1 . t1)),(T1 . t1))) by A86;

A89: (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) in card (NIC ((M /. (T2 . t2)),(T2 . t2))) by A78, A79, A85, A87, A88, FINSEQ_2:17, XXREAL_0:2;

k = (p | (Seg (n + 1))) . (len (p | (Seg (n + 1)))) by A87, FINSEQ_2:17;

hence T1 . (p | (Seg (n + 1))) = (LocSeq ((NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((p | (Seg (n + 1))) . (len (p | (Seg (n + 1))))) by A14, A84, A88

.= T2 . (p | (Seg (n + 1))) by A16, A78, A79, A85, A84, A89, XXREAL_0:2 ;

:: thesis: verum

for n being Nat holds S

hence ( p in dom T1 implies T1 . p = T2 . p ) by A76; :: thesis: verum