deffunc H1( Ordinal, Ordinal) -> set = $2 +^ (A . $1);
deffunc H2( Ordinal, Ordinal-Sequence) -> set = Union $2;
set b = dom A;
A1: ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ (dom A) & fi . 0 = 0 & ( for c being Ordinal st succ c in succ (dom A) holds
fi . (succ c) = H1(c,fi . c) ) & ( for c being Ordinal st c in succ (dom A) & c <> 0 & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ (dom A) & fi . 0 = 0 & ( for C being Ordinal st succ C in succ (dom A) holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ (dom A) & C <> 0 & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ (dom A) & fi . 0 = 0 & ( for C being Ordinal st succ C in succ (dom A) holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ (dom A) & C <> 0 & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch 13();
 then consider a being Ordinal, f being Ordinal-Sequence such that
A2: ( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for c being Ordinal st succ c in succ (dom A) holds
f . (succ c) = H1(c,f . c) ) & ( for c being Ordinal st c in succ (dom A) & c <> {} & c is limit_ordinal holds
f . c = H2(c,f | c) ) ) ;
hereby :: thesis: for b1, b2 being Ordinal st ex f being Ordinal-Sequence st
( b1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) holds
b1 = b2
take a = a; :: thesis: ex f being Ordinal-Sequence st
( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) )
take f = f; :: thesis: ( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) )
thus ( a = last f & dom f = succ (dom A) & f . 0 = 0 ) by A2; :: thesis: for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n)
let n be Nat; :: thesis: ( n in dom A implies f . (n + 1) = (f . n) +^ (A . n) )
assume n in dom A ; :: thesis: f . (n + 1) = (f . n) +^ (A . n)
then succ n c= dom A by ORDINAL1:21;
then ( succ n in succ (dom A) & Segm (n + 1) = succ (Segm n) ) by NAT_1:38, ORDINAL1:22;
hence f . (n + 1) = (f . n) +^ (A . n) by A2; :: thesis: verum
end;
let a1, a2 be Ordinal; :: thesis: ( ex f being Ordinal-Sequence st
( a1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st
( a2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) implies a1 = a2 )
given f1 being Ordinal-Sequence such that A3: ( a1 = last f1 & dom f1 = succ (dom A) & f1 . 0 = 0 & ( for n being Nat st n in dom A holds
f1 . (n + 1) = (f1 . n) +^ (A . n) ) ) ; :: thesis: ( for f being Ordinal-Sequence holds
( not a2 = last f or not dom f = succ (dom A) or not f . 0 = 0 or ex n being Nat st
( n in dom A & not f . (n + 1) = (f . n) +^ (A . n) ) ) or a1 = a2 )
given f2 being Ordinal-Sequence such that A4: ( a2 = last f2 & dom f2 = succ (dom A) & f2 . 0 = 0 & ( for n being Nat st n in dom A holds
f2 . (n + 1) = (f2 . n) +^ (A . n) ) ) ; :: thesis: a1 = a2
reconsider b = dom A as finite Ordinal ;
A5: for c being Ordinal st succ c in succ b holds
f1 . (succ c) = H1(c,f1 . c)
proof
let c be Ordinal; :: thesis: ( succ c in succ b implies f1 . (succ c) = H1(c,f1 . c) )
assume succ c in succ b ; :: thesis: f1 . (succ c) = H1(c,f1 . c)
then A6: c in b by ORDINAL3:3;
then reconsider n = c as Element of omega ;
A7: Segm (n + 1) = succ (Segm n) by NAT_1:38;
f1 . (n + 1) = H1(n,f1 . n) by A3, A6;
hence f1 . (succ c) = H1(c,f1 . c) by A7; :: thesis: verum
end;
A8: for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
f1 . c = H2(c,f1 | c)
proof
A9: succ b in omega by ORDINAL1:def 12;
let c be Ordinal; :: thesis: ( c in succ b & c <> {} & c is limit_ordinal implies f1 . c = H2(c,f1 | c) )
assume A10: ( c in succ b & c <> {} & c is limit_ordinal ) ; :: thesis: f1 . c = H2(c,f1 | c)
then 0 in c by ORDINAL3:8;
then ( c in omega & omega c= c ) by A10, ORDINAL1:10, ORDINAL1:def 11, A9;
hence f1 . c = H2(c,f1 | c) ; :: thesis: verum
end;
A11: for c being Ordinal st succ c in succ b holds
f2 . (succ c) = H1(c,f2 . c)
proof
let c be Ordinal; :: thesis: ( succ c in succ b implies f2 . (succ c) = H1(c,f2 . c) )
assume succ c in succ b ; :: thesis: f2 . (succ c) = H1(c,f2 . c)
then A12: c in b by ORDINAL3:3;
then reconsider n = c as Element of omega ;
A13: Segm (n + 1) = succ (Segm n) by NAT_1:38;
f2 . (n + 1) = H1(n,f2 . n) by A4, A12;
hence f2 . (succ c) = H1(c,f2 . c) by A13; :: thesis: verum
end;
for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
f2 . c = H2(c,f2 | c)
proof
let c be Ordinal; :: thesis: ( c in succ b & c <> {} & c is limit_ordinal implies f2 . c = H2(c,f2 | c) )
A14: succ b in omega by ORDINAL1:def 12;
assume A15: ( c in succ b & c <> {} & c is limit_ordinal ) ; :: thesis: f2 . c = H2(c,f2 | c)
then 0 in c by ORDINAL3:8;
then ( c in omega & omega c= c ) by A15, ORDINAL1:10, ORDINAL1:def 11, A14;
hence f2 . c = H2(c,f2 | c) ; :: thesis: verum
end;
hence a1 = a2 by A1, A3, A4, A5, A8, A11; :: thesis: verum