deffunc H_{1}( object ) -> set = ($1 |-- A) . x;

A1: for v being object st v in the carrier of V holds

H_{1}(v) in the carrier of R^1

A2: for v being object st v in the carrier of V holds

f . v = H_{1}(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

A1: for v being object st v in the carrier of V holds

H

proof

consider f being Function of V,R^1 such that
let v be object ; :: thesis: ( v in the carrier of V implies H_{1}(v) in the carrier of R^1 )

assume v in the carrier of V ; :: thesis: H_{1}(v) in the carrier of R^1

set vA = v |-- A;

end;assume v in the carrier of V ; :: thesis: H

set vA = v |-- A;

A2: for v being object st v in the carrier of V holds

f . v = H

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