X1: ( B is linearly-independent & Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;
defpred S1[ Element of V, object ] means ex L being Linear_Combination of B st
( $1 = Sum L & $2 = L . u );
A1: for v being Element of V ex r being Element of INT.Ring st S1[v,r]
proof
let v be Element of V; :: thesis: ex r being Element of INT.Ring st S1[v,r]
v in Lin B by X1;
then consider Lv being Linear_Combination of B such that
A4: v = Sum Lv by ZMODUL02:64;
reconsider r = Lv . u as Element of INT.Ring ;
take r ; :: thesis: S1[v,r]
thus S1[v,r] by A4; :: thesis: verum
end;
consider f being Function of V, the carrier of INT.Ring such that
A9: for v being Vector of V holds S1[v,f . v] from FUNCT_2:sch 3(A1);
 A10: for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f . v = Lv . u
proof
let v be Vector of V; :: thesis: for Lv being Linear_Combination of B st v = Sum Lv holds
f . v = Lv . u
let Lv be Linear_Combination of B; :: thesis: ( v = Sum Lv implies f . v = Lv . u )
assume A11: v = Sum Lv ; :: thesis: f . v = Lv . u
consider L being Linear_Combination of B such that
A12: ( v = Sum L & f . v = L . u ) by A9;
( Carrier L c= B & Carrier Lv c= B ) by VECTSP_6:def 4;
hence f . v = Lv . u by A11, A12, Th5, VECTSP_7:def 3; :: thesis: verum
end;
A15: for v1, v2 being Vector of V holds f . (v1 + v2) = (f . v1) + (f . v2)
proof
let v1, v2 be Vector of V; :: thesis: f . (v1 + v2) = (f . v1) + (f . v2)
consider Lv1 being Linear_Combination of B such that
P1: ( v1 = Sum Lv1 & f . v1 = Lv1 . u ) by A9;
consider Lv2 being Linear_Combination of B such that
P2: ( v2 = Sum Lv2 & f . v2 = Lv2 . u ) by A9;
consider Lv12 being Linear_Combination of B such that
P3: ( v1 + v2 = Sum Lv12 & f . (v1 + v2) = Lv12 . u ) by A9;
( Carrier Lv1 c= B & Carrier Lv2 c= B & Carrier Lv12 c= B ) by VECTSP_6:def 4;
then S: Lv12 = Lv1 + Lv2 by P1, P2, P3, Th6, VECTSP_7:def 3;
f . (v1 + v2) = Lv12 . u by P3
.= (Lv1 . u) + (Lv2 . u) by S, VECTSP_6:22
.= (f . v1) + (f . v2) by P1, P2 ;
hence f . (v1 + v2) = (f . v1) + (f . v2) ; :: thesis: verum
end;
A15A: f . (0. V) = f . ((0. V) + (0. V))
.= (f . (0. V)) + (f . (0. V)) by A15 ;
A16: for v being Vector of V
for r being Element of INT.Ring holds f . (r * v) = r * (f . v)
proof
let v be Vector of V; :: thesis: for r being Element of INT.Ring holds f . (r * v) = r * (f . v)
let r be Element of INT.Ring; :: thesis: f . (r * v) = r * (f . v)
per cases ( r = 0. INT.Ring or r <> 0. INT.Ring ) ;
suppose r = 0. INT.Ring ; :: thesis: f . (r * v) = r * (f . v)
hence f . (r * v) = r * (f . v) by A15A, ZMODUL01:1; :: thesis: verum
end;
suppose A162: r <> 0. INT.Ring ; :: thesis: f . (r * v) = r * (f . v)
consider Lv being Linear_Combination of B such that
P1: ( v = Sum Lv & f . v = Lv . u ) by A9;
consider rLv being Linear_Combination of B such that
P2: ( r * v = Sum rLv & f . (r * v) = rLv . u ) by A9;
( Carrier Lv c= B & Carrier rLv c= B ) by VECTSP_6:def 4;
then r * Lv = rLv by A162, P1, P2, Th7, VECTSP_7:def 3;
hence f . (r * v) = r * (f . v) by P1, P2, VECTSP_6:def 9; :: thesis: verum
end;
end;
end;
take f ; :: thesis: ( ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & f . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f . v = Lv . u ) & ( for v1, v2 being Vector of V holds f . (v1 + v2) = (f . v1) + (f . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds f . (r * v) = r * (f . v) ) )
thus ( ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & f . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
f . v = Lv . u ) & ( for v1, v2 being Vector of V holds f . (v1 + v2) = (f . v1) + (f . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds f . (r * v) = r * (f . v) ) ) by A9, A10, A15, A16; :: thesis: verum