let f be Point of (DualSp (DualSp X)); :: thesis:
consider x being object such that
A2: ( x in dom (BidualFunc X) & f = (BidualFunc X) . x ) by A1, FUNCT_1:def 3;
reconsider x = x as Point of X by A2;
take x ; :: thesis:
f = BiDual x by A2, Def2;
hence for g being Point of (DualSp X) holds f . g = g . x by Def1; :: thesis:

end;

assume B1: for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x ; :: thesis:
for v being object st v in the carrier of (DualSp (DualSp X)) holds
ex s being object st
( s in the carrier of X & v = (BidualFunc X) . s )

let v be object ; :: thesis:
assume v in the carrier of (DualSp (DualSp X)) ; :: thesis:
then reconsider f = v as Point of (DualSp (DualSp X)) ;
consider s being Point of X such that
B2: for g being Point of (DualSp X) holds f . g = g . s by B1;
take s ; :: thesis:
thus s in the carrier of X ; :: thesis:
f = BiDual s by B2, Def1;
hence v = (BidualFunc X) . s by Def2; :: thesis:

end;