defpred S1[ Element of NAT , Nat] means $1 in card (NIC (M /. $2),$2);
reconsider n = FirstLoc M as Element of NAT ;
defpred S2[ set , Element of NAT , set ] means ex l being Element of 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 S2[x,y,z]
proof
let x, y be Element of NAT ; :: thesis: ex z being Element of NAT st S2[x,y,z]
set z = (LocSeq (NIC (M /. x),x),S) . y;
per cases ( y in dom (LocSeq (NIC (M /. x),x),S) or not y in dom (LocSeq (NIC (M /. x),x),S) ) ;
suppose A2: y in dom (LocSeq (NIC (M /. x),x),S) ; :: thesis: ex z being Element of NAT st S2[x,y,z]
take (LocSeq (NIC (M /. x),x),S) . y ; :: thesis: ( (LocSeq (NIC (M /. x),x),S) . y is Element of NAT & S2[x,y,(LocSeq (NIC (M /. x),x),S) . y] )
A3: rng (LocSeq (NIC (M /. x),x),S) c= NAT by RELAT_1:def 19;
(LocSeq (NIC (M /. x),x),S) . y in rng (LocSeq (NIC (M /. x),x),S) by A2, FUNCT_1:def 5;
hence ( (LocSeq (NIC (M /. x),x),S) . y is Element of NAT & S2[x,y,(LocSeq (NIC (M /. x),x),S) . y] ) by A2, A3; :: thesis: verum
end;
suppose A4: not y in dom (LocSeq (NIC (M /. x),x),S) ; :: thesis: ex z being Element of NAT st S2[x,y,z]
reconsider il = 0 as Element of NAT ;
take il ; :: thesis: S2[x,y,il]
thus S2[x,y,il] by A4; :: thesis: verum
end;
end;
end;
consider f being Function of [:NAT ,NAT :],NAT such that
A5: for l, n being Element of NAT holds S2[l,n,f . l,n] from BINOP_1:sch 3(A1);
 A6: for d, k1, k2 being Element of NAT st k1 <= k2 & S1[k2,d] holds
S1[k1,d]
proof
let d be Element of NAT ; :: thesis: for k1, k2 being Element of NAT st k1 <= k2 & S1[k2,d] holds
S1[k1,d]
let k1, k2 be Element of NAT ; :: thesis: ( k1 <= k2 & S1[k2,d] implies S1[k1,d] )
assume that
A7: k1 <= k2 and
A8: S1[k2,d] ; :: thesis: S1[k1,d]
k1 c= k2 by A7, NAT_1:40;
hence S1[k1,d] by A8, ORDINAL1:22; :: thesis: verum
end;
consider T being DecoratedTree of NAT such that
A9: T . {} = n and
A10: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : S1[k,T . t] } & ( for n being Element of NAT st S1[n,T . t] holds
T . (t ^ <*n*>) = f . (T . t),n ) ) from TREES_2:sch 10(A6);
 take T ; :: thesis: ( T . {} = FirstLoc M & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (M /. (T . t)),(T . t)) } & ( for m being Element of 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 A9; :: thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (M /. (T . t)),(T . t)) } & ( for m being Element of 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 Element of NAT : k in card (NIC (M /. (T . t)),(T . t)) } & ( for m being Element of 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 Element of NAT : S1[k,T . t] } by A10; :: thesis: for m being Element of 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 Element of NAT ; :: thesis: ( m in card (NIC (M /. (T . t)),(T . t)) implies T . (t ^ <*m*>) = (LocSeq (NIC (M /. (T . t)),(T . t)),S) . m )
consider l being Element of NAT such that
A13: l = n and
A14: ( 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 A5;
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 A10, A13, A14, Def4; :: thesis: verum