consider f being T-Sequence such that
A1: dom f = card M and
A2: for A being Ordinal st A in card M holds
f . A = H₁(A) from ORDINAL2:sch 2();
f is NAT -valued

proof

let y be set ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in proj2 f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being set such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
H₁(x) in NAT ;
hence y in NAT by A1, A2, A3; :: thesis: verum

end;

then reconsider f = f as T-Sequence of NAT ;
take f ; :: thesis: ( dom f = card M & ( for m being set st m in card M holds
f . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m) ) )
thus dom f = card M by A1; :: thesis: for m being set st m in card M holds
f . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m)
let m be set ; :: thesis: ( m in card M implies f . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m) )
assume m in card M ; :: thesis: f . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m)
hence f . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m) by A2; :: thesis: verum