let L be non empty right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr ; :: thesis:
let A, B be non empty Subset of L; :: thesis:
defpred S₁[ Nat] means for f being LinearCombination of A st len f = $1 holds
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g;
assume A1: B = A \ {(0. L)} ; :: thesis:

A2: now :: thesis:

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
for f being LinearCombination of A st len f = k + 1 holds
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g

let f be LinearCombination of A; :: thesis:
set g = f | (Seg k);
reconsider g = f | (Seg k) as FinSequence by FINSEQ_1:15;
A4: rng f c= the carrier of L by FINSEQ_1:def 4;
set h = f /. (len f);
assume A5: len f = k + 1 ; :: thesis:
then 1 <= len f by NAT_1:12;
then len f in Seg (len f) by FINSEQ_1:1;
then A6: len f in dom f by FINSEQ_1:def 3;
then A7: f /. (len f) = f . (len f) by PARTFUN1:def 6;
A8: k <= k + 1 by NAT_1:12;
then A9: len g = k by A5, FINSEQ_1:17;
A10: dom g = Seg k by A5, A8, FINSEQ_1:17;
A11: dom f = Seg (k + 1) by A5, FINSEQ_1:def 3;
then A12: dom g c= dom f by A8, A10, FINSEQ_1:5;

let u be object ; :: thesis:
assume u in rng g ; :: thesis:
then consider x being object such that
A13: x in dom g and
A14: u = g . x by FUNCT_1:def 3;
g . x = f . x by A13, FUNCT_1:47;
then u in rng f by A12, A13, A14, FUNCT_1:def 3;
hence u in the carrier of L by A4; :: thesis:

end;

then rng g c= the carrier of L ;
then reconsider g = g as FinSequence of the carrier of L by FINSEQ_1:def 4;
for i being set st i in dom g holds
ex u, v being Element of L ex a being Element of A st g /. i = (u * a) * v

let i be set ; :: thesis:
assume A15: i in dom g ; :: thesis:
then reconsider i = i as Element of NAT ;
i <= k by A10, A15, FINSEQ_1:1;
then A16: i <= k + 1 by NAT_1:12;
1 <= i by A10, A15, FINSEQ_1:1;
then A17: i in dom f by A11, A16, FINSEQ_1:1;
g /. i = g . i by A15, PARTFUN1:def 6
.= f . i by A15, FUNCT_1:47
.= f /. i by A17, PARTFUN1:def 6 ;
hence ex u, v being Element of L ex a being Element of A st g /. i = (u * a) * v by A17, IDEAL_1:def 8; :: thesis:

end;

then reconsider g = g as LinearCombination of A by IDEAL_1:def 8;
consider g9 being LinearCombination of B such that
A18: Sum g = Sum g9 by A3, A9;
let u be set ; :: thesis:
assume A19: u = Sum f ; :: thesis:
A20: len f = (len g) + 1 by A5, A8, FINSEQ_1:17;
then A21: Sum f = (Sum g) + (f /. (len f)) by A10, A7, RLVECT_1:38;

case f /. (len f) = 0. L ; :: thesis:

hence Sum f = Sum g by A21, RLVECT_1:def 4; :: thesis:

end;

case A22: f /. (len f) <> 0. L ; :: thesis:

set l = g9 ^ <*(f /. (len f))*>;
for i being set st i in dom (g9 ^ <*(f /. (len f))*>) holds
ex u, v being Element of L ex a being Element of B st (g9 ^ <*(f /. (len f))*>) /. i = (u * a) * v

let i be set ; :: thesis:
assume A23: i in dom (g9 ^ <*(f /. (len f))*>) ; :: thesis:
then reconsider i = i as Element of NAT ;
A24: len (g9 ^ <*(f /. (len f))*>) = (len g9) + (len <*(f /. (len f))*>) by FINSEQ_1:22
.= (len g9) + 1 by FINSEQ_1:39 ;

case A25: i = len (g9 ^ <*(f /. (len f))*>) ; :: thesis:

consider u, v being Element of L, a being Element of A such that
A26: f /. (len f) = (u * a) * v by A6, IDEAL_1:def 8;

A27: now :: thesis:

assume not a in B ; :: thesis:
then a in {(0. L)} by A1, XBOOLE_0:def 5;
then a = 0. L by TARSKI:def 1;
then (u * a) * v = (0. L) * v
.= 0. L ;
hence contradiction by A22, A26; :: thesis:

end;

(g9 ^ <*(f /. (len f))*>) /. i = (g9 ^ <*(f /. (len f))*>) . i by A23, PARTFUN1:def 6
.= f /. (len f) by A24, A25, FINSEQ_1:42 ;
hence ex u, v being Element of L ex a being Element of B st (g9 ^ <*(f /. (len f))*>) /. i = (u * a) * v by A26, A27; :: thesis:

end;

case A28: i <> len (g9 ^ <*(f /. (len f))*>) ; :: thesis:

A29: i in Seg (len (g9 ^ <*(f /. (len f))*>)) by A23, FINSEQ_1:def 3;
then i <= len (g9 ^ <*(f /. (len f))*>) by FINSEQ_1:1;
then i < len (g9 ^ <*(f /. (len f))*>) by A28, XXREAL_0:1;
then A30: i <= len g9 by A24, NAT_1:13;
1 <= i by A29, FINSEQ_1:1;
then i in Seg (len g9) by A30, FINSEQ_1:1;
then A31: i in dom g9 by FINSEQ_1:def 3;
(g9 ^ <*(f /. (len f))*>) /. i = (g9 ^ <*(f /. (len f))*>) . i by A23, PARTFUN1:def 6
.= g9 . i by A31, FINSEQ_1:def 7
.= g9 /. i by A31, PARTFUN1:def 6 ;
hence ex u, v being Element of L ex a being Element of B st (g9 ^ <*(f /. (len f))*>) /. i = (u * a) * v by A31, IDEAL_1:def 8; :: thesis:

end;

end;

end;

hence ex u, v being Element of L ex a being Element of B st (g9 ^ <*(f /. (len f))*>) /. i = (u * a) * v ; :: thesis:

end;

then reconsider l = g9 ^ <*(f /. (len f))*> as LinearCombination of B by IDEAL_1:def 8;
Sum l = (Sum g9) + (Sum <*(f /. (len f))*>) by RLVECT_1:41
.= Sum f by A10, A18, A7, A20, RLVECT_1:38, RLVECT_1:44 ;
hence ex g being LinearCombination of B st u = Sum g by A19; :: thesis:

end;

end;

end;

hence ex g being LinearCombination of B st u = Sum g by A19, A18; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

let f be LinearCombination of A; :: thesis:
let u be set ; :: thesis:
assume A32: u = Sum f ; :: thesis:
A33: ex n being Element of NAT st len f = n ;
A34: S₁[ 0 ]

set g = <*> the carrier of L;
reconsider g = <*> the carrier of L as FinSequence of the carrier of L ;
for i being set st i in dom g holds
ex u, v being Element of L ex a being Element of B st g /. i = (u * a) * v ;
then reconsider g = g as LinearCombination of B by IDEAL_1:def 8;
let f be LinearCombination of A; :: thesis:
A35: g = <*> the carrier of L ;
assume len f = 0 ; :: thesis:
then A36: f = <*> the carrier of L ;
let u be set ; :: thesis:
assume u = Sum f ; :: thesis:
hence ex g being LinearCombination of B st u = Sum g by A36, A35; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A34, A2);
hence ex g being LinearCombination of B st u = Sum g by A32, A33; :: thesis: