deffunc H₁( VECTOR of F₁()) -> Element of NAT = 0 ;
consider f being Function of the carrier of F₁(),REAL such that
A1: f . F₂() = F₃() and
A2: for u being VECTOR of F₁() st u <> F₂() holds
f . u = H₁(u) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs the carrier of F₁(),REAL by FUNCT_2:11;

now

let u be VECTOR of F₁(); :: thesis: ( not u in {F₂()} implies f . u = 0 )
assume not u in {F₂()} ; :: thesis: f . u = 0
then u <> F₂() by TARSKI:def 1;
hence f . u = 0 by A2; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of F₁() by RLVECT_2:def 5;
Carrier f c= {F₂()}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {F₂()} )
assume that
A3: x in Carrier f and
A4: not x in {F₂()} ; :: thesis: contradiction
( f . x <> 0 & x <> F₂() ) by A3, A4, RLVECT_2:28, TARSKI:def 1;
hence contradiction by A2, A3; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {F₂()} by RLVECT_2:def 8;
take f ; :: thesis: f . F₂() = F₃()
thus f . F₂() = F₃() by A1; :: thesis: verum