defpred S_{1}[ Nat, Nat] means $1 in card (NIC ((M /. $2),$2));

reconsider n = FirstLoc M as Nat ;

defpred S_{2}[ set , Nat, set ] means ex l being Nat st

( l = $1 & ( $2 in dom (LocSeq ((NIC ((M /. l),l)),S)) implies $3 = (LocSeq ((NIC ((M /. l),l)),S)) . $2 ) & ( not $2 in dom (LocSeq ((NIC ((M /. l),l)),S)) implies $3 = 0 ) );

set D = NAT ;

A1: for x, y being Element of NAT ex z being Element of NAT st S_{2}[x,y,z]

A4: for l, n being Element of NAT holds S_{2}[l,n,f . (l,n)]
from BINOP_1:sch 3(A1);

A5: for d being Element of NAT

for k1, k2 being Nat st k1 <= k2 & S_{1}[k2,d] holds

S_{1}[k1,d]

consider T being DecoratedTree of NAT such that

A8: T . {} = n and

A9: for t being Element of dom T holds

( succ t = { (t ^ <*k*>) where k is Nat : S_{1}[k,T . t] } & ( for n being Nat st S_{1}[n,T . t] holds

T . (t ^ <*n*>) = f . ((T . t),n) ) ) from TREES_2:sch 10(A5);

take T ; :: thesis: ( T . {} = FirstLoc M & ( for t being Element of dom T holds

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

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

thus T . {} = FirstLoc M by A8; :: thesis: for t being Element of dom T holds

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

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

let t be Element of dom T; :: thesis: ( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T . t)),(T . t))) } & ( for m being Nat st m in card (NIC ((M /. (T . t)),(T . t))) holds

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

thus succ t = { (t ^ <*k*>) where k is Nat : S_{1}[k,T . t] }
by A9; :: thesis: for m being Nat st m in card (NIC ((M /. (T . t)),(T . t))) holds

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

reconsider n = T . t as Element of NAT ;

let m be Nat; :: thesis: ( m in card (NIC ((M /. (T . t)),(T . t))) implies T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m )

A10: m in NAT by ORDINAL1:def 12;

consider l being Nat such that

A11: l = n and

A12: ( m in dom (LocSeq ((NIC ((M /. l),l)),S)) implies f . (n,m) = (LocSeq ((NIC ((M /. l),l)),S)) . m ) and

( not m in dom (LocSeq ((NIC ((M /. l),l)),S)) implies f . (n,m) = 0 ) by A4, A10;

assume m in card (NIC ((M /. (T . t)),(T . t))) ; :: thesis: T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m

hence T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m by A9, A11, A12, Def1; :: thesis: verum

reconsider n = FirstLoc M as Nat ;

defpred S

( l = $1 & ( $2 in dom (LocSeq ((NIC ((M /. l),l)),S)) implies $3 = (LocSeq ((NIC ((M /. l),l)),S)) . $2 ) & ( not $2 in dom (LocSeq ((NIC ((M /. l),l)),S)) implies $3 = 0 ) );

set D = NAT ;

A1: for x, y being Element of NAT ex z being Element of NAT st S

proof

consider f being Function of [:NAT,NAT:],NAT such that
let x, y be Element of NAT ; :: thesis: ex z being Element of NAT st S_{2}[x,y,z]

reconsider z = (LocSeq ((NIC ((M /. x),x)),S)) . y as Element of NAT by ORDINAL1:def 12;

end;reconsider z = (LocSeq ((NIC ((M /. x),x)),S)) . y as Element of NAT by ORDINAL1:def 12;

per cases
( y in dom (LocSeq ((NIC ((M /. x),x)),S)) or not y in dom (LocSeq ((NIC ((M /. x),x)),S)) )
;

end;

suppose A2:
y in dom (LocSeq ((NIC ((M /. x),x)),S))
; :: thesis: ex z being Element of NAT st S_{2}[x,y,z]

end;

end;

suppose A3:
not y in dom (LocSeq ((NIC ((M /. x),x)),S))
; :: thesis: ex z being Element of NAT st S_{2}[x,y,z]

reconsider il = 0 as Element of NAT ;

take il ; :: thesis: S_{2}[x,y,il]

thus S_{2}[x,y,il]
by A3; :: thesis: verum

end;take il ; :: thesis: S

thus S

A4: for l, n being Element of NAT holds S

A5: for d being Element of NAT

for k1, k2 being Nat st k1 <= k2 & S

S

proof

reconsider n = n as Element of NAT ;
let d be Element of NAT ; :: thesis: for k1, k2 being Nat st k1 <= k2 & S_{1}[k2,d] holds

S_{1}[k1,d]

let k1, k2 be Nat; :: thesis: ( k1 <= k2 & S_{1}[k2,d] implies S_{1}[k1,d] )

assume that

A6: k1 <= k2 and

A7: S_{1}[k2,d]
; :: thesis: S_{1}[k1,d]

Segm k2 in card (NIC ((M /. d),d)) by A7;

then Segm k1 in card (NIC ((M /. d),d)) by A6, NAT_1:39, ORDINAL1:12;

hence S_{1}[k1,d]
; :: thesis: verum

end;S

let k1, k2 be Nat; :: thesis: ( k1 <= k2 & S

assume that

A6: k1 <= k2 and

A7: S

Segm k2 in card (NIC ((M /. d),d)) by A7;

then Segm k1 in card (NIC ((M /. d),d)) by A6, NAT_1:39, ORDINAL1:12;

hence S

consider T being DecoratedTree of NAT such that

A8: T . {} = n and

A9: for t being Element of dom T holds

( succ t = { (t ^ <*k*>) where k is Nat : S

T . (t ^ <*n*>) = f . ((T . t),n) ) ) from TREES_2:sch 10(A5);

take T ; :: thesis: ( T . {} = FirstLoc M & ( for t being Element of dom T holds

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

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

thus T . {} = FirstLoc M by A8; :: thesis: for t being Element of dom T holds

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

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

let t be Element of dom T; :: thesis: ( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (T . t)),(T . t))) } & ( for m being Nat st m in card (NIC ((M /. (T . t)),(T . t))) holds

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

thus succ t = { (t ^ <*k*>) where k is Nat : S

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

reconsider n = T . t as Element of NAT ;

let m be Nat; :: thesis: ( m in card (NIC ((M /. (T . t)),(T . t))) implies T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m )

A10: m in NAT by ORDINAL1:def 12;

consider l being Nat such that

A11: l = n and

A12: ( m in dom (LocSeq ((NIC ((M /. l),l)),S)) implies f . (n,m) = (LocSeq ((NIC ((M /. l),l)),S)) . m ) and

( not m in dom (LocSeq ((NIC ((M /. l),l)),S)) implies f . (n,m) = 0 ) by A4, A10;

assume m in card (NIC ((M /. (T . t)),(T . t))) ; :: thesis: T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m

hence T . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (T . t)),(T . t))),S)) . m by A9, A11, A12, Def1; :: thesis: verum