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 = H_{1}(A)
from ORDINAL2:sch 2();

f is NAT -valued

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

A1: dom f = card M and

A2: for A being Ordinal st A in card M holds

f . A = H

f is NAT -valued

proof

then reconsider f = f as Sequence of NAT ;
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;

H_{1}(x) in NAT
by ORDINAL1:def 12;

hence y in NAT by A1, A2, A3; :: thesis: verum

end;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;

H

hence y in NAT by A1, A2, A3; :: thesis: verum

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