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 3;
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:39;
hence S1[k1,d] by A8, ORDINAL1:12; :: 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
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 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, A11, A12, Def3; :: thesis: verum