let f1, f2 be Function of X,(DualSp (DualSp X)); :: thesis: ( ( for x being Point of X holds f1 . x = BiDual x ) & ( for x being Point of X holds f2 . x = BiDual x ) implies f1 = f2 )
assume A1: ( ( for x being Point of X holds f1 . x = BiDual x ) & ( for x being Point of X holds f2 . x = BiDual x ) ) ; :: thesis: f1 = f2
A3: ( dom f1 = the carrier of X & dom f2 = the carrier of X ) by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider x1 = x as Point of X ;
f1 . x = BiDual x1 by A1;
hence f1 . x = f2 . x by A1; :: thesis: verum

end;

hence f1 = f2 by A3; :: thesis: verum