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

end;

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

proof

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

end;

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