deffunc H₁( Ordinal) -> set = { ((g . b) . $1) where b is Element of dom g : b in dom g } ;
deffunc H₂( Ordinal) -> set = union (On H₁($1));
consider f being Ordinal-Sequence such that
A1: ( dom f = dom (g . 0) & ( for a being Ordinal st a in dom (g . 0) holds
f . a = H₂(a) ) ) from ORDINAL2:sch 3();
take f ; :: thesis: ( dom f = dom (g . 0) & ( for a being Ordinal st a in dom f holds
f . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) )
thus dom f = dom (g . 0) by A1; :: thesis: for a being Ordinal st a in dom f holds
f . a = union { ((g . b) . a) where b is Element of dom g : b in dom g }
let a be Ordinal; :: thesis: ( a in dom f implies f . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } )
assume a in dom f ; :: thesis: f . a = union { ((g . b) . a) where b is Element of dom g : b in dom g }
then A2: f . a = H₂(a) by A1;

now :: thesis: for x being set st x in H₁(a) holds
x is ordinal

let x be set ; :: thesis: ( x in H₁(a) implies x is ordinal )
assume x in H₁(a) ; :: thesis: x is ordinal
then ex b being Element of dom g st
( x = (g . b) . a & b in dom g ) ;
hence x is ordinal ; :: thesis: verum

end;

then H₁(a) is ordinal-membered by Th1;
hence f . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } by A2, Th2; :: thesis: verum