let A1, A2 be Ordinal; :: thesis:
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:
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:

let x be object ; :: thesis:
assume A12: x in dom L ; :: thesis:
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:

end;