consider phi being Ordinal-Sequence such that
A1: dom phi = On F1() and
A2: ( 0 in On F1() implies phi . 0 = F2() ) and
A3: for A being Ordinal st succ A in On F1() holds
phi . (succ A) = F3(A,(phi . A)) and
A4: for A being Ordinal st A in On F1() & A <> 0 & A is limit_ordinal holds
phi . A = F4(A,(phi | A)) from ORDINAL2:sch 11();
 rng phi c= On F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in On F1() )
assume x in rng phi ; :: thesis: x in On F1()
then consider y being object such that
A5: y in dom phi and
A6: x = phi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal of F1() by A1, A5, ORDINAL1:def 9;
A7: now :: thesis: ( ( for A being Ordinal holds not y = succ A ) & y <> {} implies x in On F1() )
assume for A being Ordinal holds not y = succ A ; :: thesis: ( y <> {} implies x in On F1() )
then A8: y is limit_ordinal by ORDINAL1:29;
assume y <> {} ; :: thesis: x in On F1()
then x = F4(y,(phi | y)) by A1, A4, A5, A6, A8;
hence x in On F1() by ORDINAL1:def 9; :: thesis: verum
end;
now :: thesis: ( ex A being Ordinal st y = succ A implies x in On F1() )
given A being Ordinal such that A9: y = succ A ; :: thesis: x in On F1()
reconsider B = phi . A as Ordinal ;
x = F3(A,B) by A1, A3, A5, A6, A9;
hence x in On F1() by ORDINAL1:def 9; :: thesis: verum
end;
hence x in On F1() by A2, A6, A7, ORDINAL1:def 9; :: thesis: verum
end;
then reconsider phi = phi as Ordinal-Sequence of F1() by A1, FUNCT_2:def 1, RELSET_1:4;
take phi ; :: thesis: ( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
0-element_of F1() in dom phi by ORDINAL4:34;
hence phi . (0-element_of F1()) = F2() by A1, A2, ORDINAL4:33; :: thesis: ( ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
thus for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) by A1, A3, ORDINAL4:34; :: thesis: for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a))
let a be Ordinal of F1(); :: thesis: ( a <> 0-element_of F1() & a is limit_ordinal implies phi . a = F4(a,(phi | a)) )
( a in dom phi & {} = 0-element_of F1() ) by ORDINAL4:33, ORDINAL4:34;
hence ( a <> 0-element_of F1() & a is limit_ordinal implies phi . a = F4(a,(phi | a)) ) by A4; :: thesis: verum