let F1, F2 be Point of (DualSp (DualSp X)); :: thesis: ( ( for f being Point of (DualSp X) holds F1 . f = f . x ) & ( for f being Point of (DualSp X) holds F2 . f = f . x ) implies F1 = F2 )
assume A1: ( ( for f being Point of (DualSp X) holds F1 . f = f . x ) & ( for f being Point of (DualSp X) holds F2 . f = f . x ) ) ; :: thesis: F1 = F2
A2: ( F1 is Lipschitzian linear-Functional of (DualSp X) & F2 is Lipschitzian linear-Functional of (DualSp X) ) by DUALSP01:def 10;
then A3: ( dom F1 = the carrier of (DualSp X) & dom F2 = the carrier of (DualSp X) ) by FUNCT_2:def 1;
now :: thesis: for f being object st f in dom F1 holds
F1 . f = F2 . f
let f be object ; :: thesis: ( f in dom F1 implies F1 . f = F2 . f )
assume f in dom F1 ; :: thesis: F1 . f = F2 . f
then reconsider f1 = f as Point of (DualSp X) by A2, FUNCT_2:def 1;
F1 . f = f1 . x by A1;
hence F1 . f = F2 . f by A1; :: thesis: verum
end;
hence F1 = F2 by A3; :: thesis: verum