deffunc H₁( Element of X) -> Point of (DualSp (DualSp X)) = BiDual $1;
ex f being Function of X,(DualSp (DualSp X)) st
for x being Element of the carrier of X holds f . x = H₁(x) from FUNCT_2:sch 4();
then consider f being Function of X,(DualSp (DualSp X)) such that
P1: for x being Point of X holds f . x = BiDual x ;
take f ; :: thesis: for x being Point of X holds f . x = BiDual x
thus for x being Point of X holds f . x = BiDual x by P1; :: thesis: verum