let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for LG being Linear_Combination of G
for g being Element of G holds sum LG = sum (g + LG)
let LG be Linear_Combination of G; :: thesis: for g being Element of G holds sum LG = sum (g + LG)
let g be Element of G; :: thesis: sum LG = sum (g + LG)
set gL = g + LG;
deffunc H₁( Element of G) -> Element of the carrier of G = $1 + g;
consider f being Function of the carrier of G, the carrier of G such that
A1: for h being Element of G holds f . h = H₁(h) from FUNCT_2:sch 4();
consider F being FinSequence of G such that
A2: F is one-to-one and
A3: rng F = Carrier LG and
A4: sum LG = Sum (LG * F) by Def3;
A5: len (f * F) = len F by FINSEQ_2:33;
A6: len (LG * F) = len F by FINSEQ_2:33;
A7: len ((g + LG) * (f * F)) = len (f * F) by FINSEQ_2:33;

A8: now :: thesis: for k being Nat st 1 <= k & k <= len F holds
((g + LG) * (f * F)) . k = (LG * F) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len F implies ((g + LG) * (f * F)) . k = (LG * F) . k )
assume A9: ( 1 <= k & k <= len F ) ; :: thesis: ((g + LG) * (f * F)) . k = (LG * F) . k
then k in dom F by FINSEQ_3:25;
then A10: F /. k = F . k by PARTFUN1:def 6;
k in dom (LG * F) by A6, A9, FINSEQ_3:25;
then A11: (LG * F) . k = LG . (F . k) by FUNCT_1:12;
k in dom ((g + LG) * (f * F)) by A5, A7, A9, FINSEQ_3:25;
then A12: ((g + LG) * (f * F)) . k = (g + LG) . ((f * F) . k) by FUNCT_1:12;
k in dom (f * F) by A5, A9, FINSEQ_3:25;
then (f * F) . k = f . (F . k) by FUNCT_1:12;
then (f * F) . k = (F /. k) + g by A1, A10;
hence ((g + LG) * (f * F)) . k = LG . (((F /. k) + g) - g) by A12, Def1
.= LG . (((F /. k) + g) + (- g)) by RLVECT_1:def 11
.= LG . ((F /. k) + (g + (- g))) by RLVECT_1:def 3
.= LG . ((F /. k) + (0. G)) by RLVECT_1:def 10
.= (LG * F) . k by A10, A11 ;
:: thesis: verum

end;

now :: thesis: for x1, x2 being object st x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 implies x1 = x2 )
assume that
A13: x1 in dom (f * F) and
A14: x2 in dom (f * F) and
A15: (f * F) . x1 = (f * F) . x2 ; :: thesis: x1 = x2
A16: f . (F /. x1) = (F /. x1) + g by A1;
A17: x1 in dom F by A13, FUNCT_1:11;
then A18: F . x1 = F /. x1 by PARTFUN1:def 6;
A19: x2 in dom F by A14, FUNCT_1:11;
then A20: F . x2 = F /. x2 by PARTFUN1:def 6;
( (f * F) . x1 = f . (F . x1) & (f * F) . x2 = f . (F . x2) ) by A13, A14, FUNCT_1:12;
then (F /. x1) + g = (F /. x2) + g by A1, A15, A16, A18, A20;
then F /. x1 = F /. x2 by RLVECT_1:8;
hence x1 = x2 by A2, A17, A18, A19, A20, FUNCT_1:def 4; :: thesis: verum

end;

then A21: f * F is one-to-one by FUNCT_1:def 4;
Carrier (g + LG) c= rng (f * F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (g + LG) or x in rng (f * F) )
assume x in Carrier (g + LG) ; :: thesis: x in rng (f * F)
then x in g + (Carrier LG) by Th16;
then consider h being Element of G such that
A22: x = g + h and
A23: h in Carrier LG ;
consider y being object such that
A24: y in dom F and
A25: F . y = h by A3, A23, FUNCT_1:def 3;
A26: f . (F . y) = x by A1, A22, A25;
dom f = the carrier of G by FUNCT_2:def 1;
then A27: y in dom (f * F) by A24, A25, FUNCT_1:11;
then (f * F) . y in rng (f * F) by FUNCT_1:def 3;
hence x in rng (f * F) by A26, A27, FUNCT_1:12; :: thesis: verum

end;

then sum (g + LG) = Sum ((g + LG) * (f * F)) by A21, Th30;
hence sum LG = sum (g + LG) by A4, A5, A6, A7, A8, FINSEQ_1:14; :: thesis: verum