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_{1}( 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_{1}(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;

Carrier (g + LG) c= rng (f * F)

hence sum LG = sum (g + LG) by A4, A5, A6, A7, A8, FINSEQ_1:14; :: thesis: verum

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

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

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

((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;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

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

then A21:
f * F is one-to-one
by FUNCT_1:def 4;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;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

Carrier (g + LG) c= rng (f * F)

proof

then
sum (g + LG) = Sum ((g + LG) * (f * F))
by A21, Th30;
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;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

hence sum LG = sum (g + LG) by A4, A5, A6, A7, A8, FINSEQ_1:14; :: thesis: verum