let A1, A2 be Ordinal; :: thesis: ( ex fi being Ordinal-Sequence st
( A1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( A2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) implies A1 = A2 )
given fi being Ordinal-Sequence such that A2: ( A1 = inf fi & dom fi = dom L ) and
A3: for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ; :: thesis: ( for fi being Ordinal-Sequence holds
( not A2 = inf fi or not dom fi = dom L or ex A being Ordinal st
( A in dom L & not fi . A = sup (rng (L | ((dom L) \ A))) ) ) or A1 = A2 )
given psi being Ordinal-Sequence such that A4: ( A2 = inf psi & dom psi = dom L ) and
A5: for A being Ordinal st A in dom L holds
psi . A = sup (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 A6: x in dom L ; :: thesis: fi . x = psi . x
then reconsider A = x as Ordinal ;
fi . A = sup (rng (L | ((dom L) \ A))) by A3, A6;
hence fi . x = psi . x by A5, A6; :: thesis: verum

end;

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