consider f being Sequence such that
A1: dom f = card M and
A2: for A being Ordinal st A in card M holds
f . A = H1(A) from ORDINAL2:sch 2();
 f is NAT -valued
proof
let y be object ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being object such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
H1(x) in NAT by ORDINAL1:def 12;
hence y in NAT by A1, A2, A3; :: thesis: verum
end;
then reconsider f = f as Sequence of NAT ;
take f ; :: thesis: ( dom f = card M & ( for m being set st m in card M holds
f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) )
thus dom f = card M by A1; :: thesis: for m being set st m in card M holds
f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m
let m be set ; :: thesis: ( m in card M implies f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m )
assume m in card M ; :: thesis: f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m
hence f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m by A2; :: thesis: verum