deffunc H1( Ordinal) -> set = { ((g . b) . $1) where b is Element of dom g : b in dom g } ;
deffunc H2( Ordinal) -> set = union (On H1($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 = H2(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 = H2(a) by A1;
now :: thesis: for x being set st x in H1(a) holds
x is ordinal
let x be set ; :: thesis: ( x in H1(a) implies x is ordinal )
assume x in H1(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 H1(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