deffunc H₁( Ordinal, Ordinal) -> set = $2 +^ (A . $1);
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = Union $2;
set b = dom A;
A0: ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ (dom A) & fi . {} = 0 & ( for c being Ordinal st succ c in succ (dom A) holds
fi . (succ c) = H₁(c,fi . c) ) & ( for c being Ordinal st c in succ (dom A) & c <> {} & c is limit_ordinal holds
fi . c = H₂(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 & ( for C being Ordinal st succ C in succ (dom A) holds
fi . (succ C) = H₁(C,fi . C) ) & ( for C being Ordinal st C in succ (dom A) & C <> {} & C is limit_ordinal holds
fi . C = H₂(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ (dom A) & fi . {} = 0 & ( for C being Ordinal st succ C in succ (dom A) holds
fi . (succ C) = H₁(C,fi . C) ) & ( for C being Ordinal st C in succ (dom A) & C <> {} & C is limit_ordinal holds
fi . C = H₂(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch 13();
then consider a being ordinal number , 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) = H₁(c,f . c) ) & ( for c being Ordinal st c in succ (dom A) & c <> {} & c is limit_ordinal holds
f . c = H₂(c,f | c) ) ) ;

hereby :: thesis: for b₁, b₂ being Ordinal st ex f being Ordinal-Sequence st
( b₁ = 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
( b₂ = 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
b₁ = b₂

take a = a; :: thesis: ex f being Ordinal-Sequence st
( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being natural number 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 natural number 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 natural number st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n)
let n be natural number ; :: 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:33;
then ( succ n in succ (dom A) & n + 1 = succ n ) by ORDINAL1:34, NAT_1:39;
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 B1: ( 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 B2: ( 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 ;
A3: ( succ b in omega & b in omega ) by CARD_1:103;
B3: for c being Ordinal st succ c in succ b holds
f1 . (succ c) = H₁(c,f1 . c)

proof

let c be ordinal number ; :: thesis: ( succ c in succ b implies f1 . (succ c) = H₁(c,f1 . c) )
assume succ c in succ b ; :: thesis: f1 . (succ c) = H₁(c,f1 . c)
then Z0: c in b by ORDINAL3:5;
then reconsider n = c as Element of omega ;
f1 . (n + 1) = H₁(n,f1 . n) by B1, Z0;
hence f1 . (succ c) = H₁(c,f1 . c) by NAT_1:39; :: thesis: verum

end;

B4: for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
f1 . c = H₂(c,f1 | c)

proof

let c be Ordinal; :: thesis: ( c in succ b & c <> {} & c is limit_ordinal implies f1 . c = H₂(c,f1 | c) )
assume C0: ( c in succ b & c <> {} & c is limit_ordinal ) ; :: thesis: f1 . c = H₂(c,f1 | c)
then 0 in c by ORDINAL3:10;
then ( c in omega & omega c= c ) by C0, A3, ORDINAL1:19, ORDINAL1:def 12;
hence f1 . c = H₂(c,f1 | c) ; :: thesis: verum

end;

B5: for c being Ordinal st succ c in succ b holds
f2 . (succ c) = H₁(c,f2 . c)

proof

let c be ordinal number ; :: thesis: ( succ c in succ b implies f2 . (succ c) = H₁(c,f2 . c) )
assume succ c in succ b ; :: thesis: f2 . (succ c) = H₁(c,f2 . c)
then Z0: c in b by ORDINAL3:5;
then reconsider n = c as Element of omega ;
f2 . (n + 1) = H₁(n,f2 . n) by B2, Z0;
hence f2 . (succ c) = H₁(c,f2 . c) by NAT_1:39; :: thesis: verum

end;

for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
f2 . c = H₂(c,f2 | c)

proof

let c be Ordinal; :: thesis: ( c in succ b & c <> {} & c is limit_ordinal implies f2 . c = H₂(c,f2 | c) )
assume C0: ( c in succ b & c <> {} & c is limit_ordinal ) ; :: thesis: f2 . c = H₂(c,f2 | c)
then 0 in c by ORDINAL3:10;
then ( c in omega & omega c= c ) by C0, A3, ORDINAL1:19, ORDINAL1:def 12;
hence f2 . c = H₂(c,f2 | c) ; :: thesis: verum

end;

hence a1 = a2 by A0, B1, B2, B3, B4, B5; :: thesis: verum