deffunc H₁( VECTOR of F₁()) -> Element of NAT = 0 ;
consider f being Function of the carrier of F₁(),REAL such that
A4: ( f . F₂() = F₅() & f . F₃() = F₆() & f . F₄() = F₇() ) and
A5: for u being VECTOR of F₁() st u <> F₂() & u <> F₃() & u <> F₄() holds
f . u = H₁(u) from RLVECT_4:sch 1(A1, A2, A3);
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₂(),F₃(),F₄()} implies f . u = 0 )
assume A6: not u in {F₂(),F₃(),F₄()} ; :: thesis: f . u = 0
then A7: u <> F₄() by ENUMSET1:def 1;
( u <> F₂() & u <> F₃() ) by A6, ENUMSET1:def 1;
hence f . u = 0 by A5, A7; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {F₂(),F₃(),F₄()} )
assume that
A8: x in Carrier f and
A9: not x in {F₂(),F₃(),F₄()} ; :: thesis: contradiction
A10: ( x <> F₃() & x <> F₄() ) by A9, ENUMSET1:def 1;
( f . x <> 0 & x <> F₂() ) by A8, A9, ENUMSET1:def 1, RLVECT_2:28;
hence contradiction by A5, A8, A10; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {F₂(),F₃(),F₄()} by RLVECT_2:def 8;
take f ; :: thesis: ( f . F₂() = F₅() & f . F₃() = F₆() & f . F₄() = F₇() )
thus ( f . F₂() = F₅() & f . F₃() = F₆() & f . F₄() = F₇() ) by A4; :: thesis: verum