let L be non empty right_complementable associative well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr ; :: thesis: for A, B being non empty Subset of L st 0. L in A & B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
let A, B be non empty Subset of L; :: thesis: ( 0. L in A & B = A \ {(0. L)} implies for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g )
assume A1:
( 0. L in A & B = A \ {(0. L)} )
; :: thesis: for f being LinearCombination of A
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: for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
let u be set ; :: thesis: ( u = Sum f implies ex g being LinearCombination of B st u = Sum g )
assume A2:
u = Sum f
; :: thesis: ex g being LinearCombination of B st u = Sum g
defpred S1[ Element of 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;
A3:
S1[ 0 ]
A7:
now let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )assume A8:
S1[
k]
;
:: thesis: S1[k + 1]
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
proof
let f be
LinearCombination of
A;
:: thesis: ( len f = k + 1 implies for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g )
assume A9:
len f = k + 1
;
:: thesis: for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
let u be
set ;
:: thesis: ( u = Sum f implies ex g being LinearCombination of B st u = Sum g )
assume A10:
u = Sum f
;
:: thesis: ex g being LinearCombination of B st u = Sum g
set g =
f | (Seg k);
reconsider g =
f | (Seg k) as
FinSequence by FINSEQ_1:19;
A11:
rng f c= the
carrier of
L
by FINSEQ_1:def 4;
A12:
k <= k + 1
by NAT_1:12;
then A13:
len g = k
by A9, FINSEQ_1:21;
A14:
dom g = Seg k
by A9, A12, FINSEQ_1:21;
A15:
dom f = Seg (k + 1)
by A9, FINSEQ_1:def 3;
then A16:
dom g c= dom f
by A12, A14, FINSEQ_1:7;
then
rng g c= the
carrier of
L
by TARSKI:def 3;
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
proof
let i be
set ;
:: thesis: ( i in dom g implies ex u, v being Element of L ex a being Element of A st g /. i = (u * a) * v )
assume A18:
i in dom g
;
:: thesis: ex u, v being Element of L ex a being Element of A st g /. i = (u * a) * v
then reconsider i =
i as
Element of
NAT ;
( 1
<= i &
i <= k )
by A14, A18, FINSEQ_1:3;
then
( 1
<= i &
i <= k + 1 )
by NAT_1:12;
then A19:
i in dom f
by A15, FINSEQ_1:3;
then consider u,
v being
Element of
L,
a being
Element of
A such that A20:
f /. i = (u * a) * v
by IDEAL_1:def 9;
g /. i =
g . i
by A18, PARTFUN1:def 8
.=
f . i
by A18, FUNCT_1:70
.=
f /. i
by A19, PARTFUN1:def 8
;
hence
ex
u,
v being
Element of
L ex
a being
Element of
A st
g /. i = (u * a) * v
by A20;
:: thesis: verum
end;
then reconsider g =
g as
LinearCombination of
A by IDEAL_1:def 9;
consider g' being
LinearCombination of
B such that A21:
Sum g = Sum g'
by A8, A13;
set h =
f /. (len f);
1
<= len f
by A9, NAT_1:12;
then
len f in Seg (len f)
by FINSEQ_1:3;
then A22:
len f in dom f
by FINSEQ_1:def 3;
then A23:
f /. (len f) = f . (len f)
by PARTFUN1:def 8;
A24:
len f = (len g) + 1
by A9, A12, FINSEQ_1:21;
then A25:
Sum f = (Sum g) + (f /. (len f))
by A14, A23, RLVECT_1:55;
hence
ex
g being
LinearCombination of
B st
u = Sum g
by A10, A21;
:: thesis: verum
end; hence
S1[
k + 1]
;
:: thesis: verum end;
A34:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A3, A7);
consider n being Element of NAT such that
A35:
len f = n
;
thus
ex g being LinearCombination of B st u = Sum g
by A2, A34, A35; :: thesis: verum