deffunc H₁( object ) -> set = ($1 |-- A) . x;
A1: for v being object st v in the carrier of V holds
H₁(v) in the carrier of R^1

proof

let v be object ; :: thesis: ( v in the carrier of V implies H₁(v) in the carrier of R^1 )
assume v in the carrier of V ; :: thesis: H₁(v) in the carrier of R^1
set vA = v |-- A;

per cases ( x in dom (v |-- A) or not x in dom (v |-- A) ) ;

suppose x in dom (v |-- A) ; :: thesis: H₁(v) in the carrier of R^1

then (v |-- A) . x in rng (v |-- A) by FUNCT_1:def 3;
hence H₁(v) in the carrier of R^1 by TOPMETR:17; :: thesis: verum

end;

suppose not x in dom (v |-- A) ; :: thesis: H₁(v) in the carrier of R^1

then (v |-- A) . x = 0 by FUNCT_1:def 2;
hence H₁(v) in the carrier of R^1 by Lm5, TOPMETR:17; :: thesis: verum

end;

end;

end;

consider f being Function of V,R^1 such that
A2: for v being object st v in the carrier of V holds
f . v = H₁(v) from FUNCT_2:sch 2(A1);
take f ; :: thesis: for v being VECTOR of V holds f . v = (v |-- A) . x
let v be Element of V; :: thesis: f . v = (v |-- A) . x
thus f . v = (v |-- A) . x by A2; :: thesis: verum