deffunc H1( Ordinal, Ordinal-Sequence) -> Ordinal = lim $2;
deffunc H2( Ordinal, Ordinal) -> Ordinal = A *^ $2;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & 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 B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & 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 B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & 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 B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2 ) )
; verum