deffunc H_{1}( Element of G) -> Element of the carrier of G = g + $1;

set vC = { H_{1}(h) where h is Element of G : h in Carrier LG } ;

A1: { H_{1}(h) where h is Element of G : h in Carrier LG } c= the carrier of G

{ H_{1}(h) where h is Element of G : h in Carrier LG } is finite
from FRAENKEL:sch 21(A2);

then reconsider vC = { H_{1}(h) where h is Element of G : h in Carrier LG } as finite Subset of G by A1;

deffunc H_{2}( 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 = H_{2}(h)
from FUNCT_2:sch 4();

reconsider f = f as Element of Funcs ( the carrier of G,REAL) by FUNCT_2:8;

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

set vC = { H

A1: { H

proof

A2:
Carrier LG is finite
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(h) where h is Element of G : h in Carrier LG } or x in the carrier of G )

assume x in { H_{1}(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 = H_{1}(h) & h in Carrier LG )
;

hence x in the carrier of G ; :: thesis: verum

end;assume x in { H

then ex h being Element of G st

( x = H

hence x in the carrier of G ; :: thesis: verum

{ H

then reconsider vC = { H

deffunc H

consider f being Function of the carrier of G,REAL such that

A3: for h being Element of G holds f . h = H

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

then reconsider f = f as Linear_Combination of G by RLVECT_2:def 3;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;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

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