deffunc H1( Ordinal, Ordinal-Sequence) -> set = union (sup $2);
deffunc H2( Ordinal, Ordinal) -> Ordinal = $2 +^ B;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) )
from ORDINAL2:sch 13();
hence
( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . 0 = 0 & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2 ) )
; verum