defpred S1[ Nat, Nat] means $1 in card (NIC ((M /. $2),$2));
reconsider n = FirstLoc M as Nat ;
defpred S2[ 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 S2[x,y,z]
proof
let x, y be Element of NAT ; :: thesis: ex z being Element of NAT st S2[x,y,z]
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)) ) ;
suppose A2: y in dom (LocSeq ((NIC ((M /. x),x)),S)) ; :: thesis: ex z being Element of NAT st S2[x,y,z]
take z ; :: thesis: S2[x,y,z]
thus S2[x,y,z] by A2; :: thesis: verum
end;
suppose A3: 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 A3; :: thesis: verum
end;
end;
end;
consider f being Function of [:NAT,NAT:],NAT such that
A4: for l, n being Element of NAT holds S2[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 & S1[k2,d] holds
S1[k1,d]
proof
let d be Element of NAT ; :: thesis: for k1, k2 being Nat st k1 <= k2 & S1[k2,d] holds
S1[k1,d]
let k1, k2 be Nat; :: thesis: ( k1 <= k2 & S1[k2,d] implies S1[k1,d] )
assume that
A6: k1 <= k2 and
A7: S1[k2,d] ; :: thesis: S1[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 S1[k1,d] ; :: thesis: verum
end;
reconsider n = n as Element of NAT ;
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 : S1[k,T . t] } & ( for n being Nat st S1[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 : S1[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