deffunc H1( Element of G) -> Element of the carrier of G = g + $1;
set vC = { H1(h) where h is Element of G : h in Carrier LG } ;
A1: { H1(h) where h is Element of G : h in Carrier LG } c= the carrier of G
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(h) where h is Element of G : h in Carrier LG } or x in the carrier of G )
assume x in { H1(h) where h is Element of G : h in Carrier LG } ; :: thesis: x in the carrier of G
then ex h being Element of G st
( x = H1(h) & h in Carrier LG ) ;
hence x in the carrier of G ; :: thesis: verum
end;
A2: Carrier LG is finite ;
{ H1(h) where h is Element of G : h in Carrier LG } is finite from FRAENKEL:sch 21(A2);
 then reconsider vC = { H1(h) where h is Element of G : h in Carrier LG } as finite Subset of G by A1;
deffunc H2( Element of G) -> Element of REAL = LG . ($1 - g);
consider f being Function of the carrier of G,REAL such that
A3: for h being Element of G holds f . h = H2(h) from FUNCT_2:sch 4();
 reconsider f = f as Element of Funcs ( the carrier of G,REAL) by FUNCT_2:8;
now :: thesis: for h being Element of G st not h in vC holds
not f . h <> 0
let h be Element of G; :: thesis: ( not h in vC implies not f . h <> 0 )
assume A4: not h in vC ; :: thesis: not f . h <> 0
assume f . h <> 0 ; :: thesis: contradiction
then LG . (h - g) <> 0 by A3;
then A5: h - g in Carrier LG ;
g + (h - g) = (h + (- g)) + g by RLVECT_1:def 11
.= h + (g + (- g)) by RLVECT_1:def 3
.= h + (0. G) by RLVECT_1:def 10
.= h ;
hence contradiction by A4, A5; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of G by RLVECT_2:def 3;
take f ; :: thesis: for h being Element of G holds f . h = LG . (h - g)
thus for h being Element of G holds f . h = LG . (h - g) by A3; :: thesis: verum