let A1, A2 be Ordinal; :: thesis: ( ex fi being Ordinal-Sequence st
( A1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( A2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) implies A1 = A2 )
given fi being Ordinal-Sequence such that A8: A1 = sup fi and
A9: ( dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) ; :: thesis: ( for fi being Ordinal-Sequence holds
( not A2 = sup fi or not dom fi = dom L or ex A being Ordinal st
( A in dom L & not fi . A = inf (rng (L | ((dom L) \ A))) ) ) or A1 = A2 )
given psi being Ordinal-Sequence such that A10: A2 = sup psi and
A11: ( dom psi = dom L & ( for A being Ordinal st A in dom L holds
psi . A = inf (rng (L | ((dom L) \ A))) ) ) ; :: thesis: A1 = A2

now

let x be set ; :: thesis: ( x in dom L implies fi . x = psi . x )
assume A12: x in dom L ; :: thesis: fi . x = psi . x
then reconsider A = x as Ordinal ;
( fi . A = inf (rng (L | ((dom L) \ A))) & psi . A = inf (rng (L | ((dom L) \ A))) ) by A9, A11, A12;
hence fi . x = psi . x ; :: thesis: verum

end;

hence A1 = A2 by A8, A9, A10, A11, FUNCT_1:9; :: thesis: verum