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 & dom fi = dom L ) and
A9: 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 & dom psi = dom L ) and
A11: for A being Ordinal st A in dom L holds
psi . A = inf (rng (L | ((dom L) \ A))) ; :: thesis: A1 = A2

now :: thesis: for x being object st x in dom L holds
fi . x = psi . x

let x be object ; :: 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))) by A9, A12;
hence fi . x = psi . x by A11, A12; :: thesis: verum

end;

hence A1 = A2 by A8, A10, FUNCT_1:2; :: thesis: verum