consider f being Sequence such that
A1: ( dom f = succ alpha & ( for beta being Ordinal
for f1 being Sequence st beta in succ alpha & f1 = f | beta holds
f . beta = H₁(f1) ) ) from ORDINAL1:sch 4();
take f . alpha ; :: thesis: ex f being Sequence st
( alpha in dom f & f . alpha = f . alpha & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) )
take f ; :: thesis: ( alpha in dom f & f . alpha = f . alpha & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) )
thus alpha in dom f by A1, ORDINAL1:6; :: thesis: ( f . alpha = f . alpha & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) )
thus ( f . alpha = f . alpha & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) by A1; :: thesis: verum