per cases ( B = {} or B <> {} ) ;

suppose AS: B = {} ; :: thesis: ex b₁ being linear-transformation of U,V st b₁ | B = f

deffunc H₁( object ) -> Element of the carrier of V = 0. V;
H2: for x being object st x in the carrier of U holds
H₁(x) in the carrier of V ;
consider T being Function of the carrier of U, the carrier of V such that
A: for u being object st u in the carrier of U holds
T . u = H₁(u) from FUNCT_2:sch 2(H2);

now :: thesis: for u1, u2 being Element of U holds (T . u1) + (T . u2) = T . (u1 + u2)

let u1, u2 be Element of U; :: thesis: (T . u1) + (T . u2) = T . (u1 + u2)
thus (T . u1) + (T . u2) = (0. V) + (T . u2) by A
.= (0. V) + (0. V) by A
.= T . (u1 + u2) by A ; :: thesis: verum

end;

then B: T is additive by VECTSP_1:def 20;

now :: thesis: for a being Element of F
for u being Element of U holds a * (T . u) = T . (a * u)

let a be Element of F; :: thesis: for u being Element of U holds a * (T . u) = T . (a * u)
let u be Element of U; :: thesis: a * (T . u) = T . (a * u)
thus a * (T . u) = a * (0. V) by A
.= 0. V by VECTSP_1:14
.= T . (a * u) by A ; :: thesis: verum

end;

then C: T is homogeneous by MOD_2:def 2;
B c= the carrier of U ;
then B c= dom T by FUNCT_2:def 1;
then (dom T) /\ B = B by XBOOLE_1:28
.= dom f by FUNCT_2:def 1 ;
then T | B = f by AS;
hence ex b₁ being linear-transformation of U,V st b₁ | B = f by B, C; :: thesis: verum

end;

suppose H: B <> {} ; :: thesis: ex b₁ being linear-transformation of U,V st b₁ | B = f

then reconsider B1 = B as non empty finite Subset of U ;
reconsider f = f as Function of B1,V ;
B: Lin B = ModuleStr(# the carrier of U, the addF of U, the ZeroF of U, the lmult of U #) by VECTSP_7:def 3;
defpred S₁[ object , object ] means for l being Linear_Combination of B1 st $1 = Sum l holds
$2 = Sum (f (#) l);

AA: now :: thesis: for x being object st x in the carrier of U holds
ex y being object st
( y in the carrier of V & S₁[x,y] )

let x be object ; :: thesis: ( x in the carrier of U implies ex y being object st
( y in the carrier of V & S₁[x,y] ) )
assume x in the carrier of U ; :: thesis: ex y being object st
( y in the carrier of V & S₁[x,y] )
then reconsider u = x as Element of U ;
u in the carrier of (Lin B) by B;
then u in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l being Linear_Combination of B1 such that
C1: u = Sum l ;
thus ex y being object st
( y in the carrier of V & S₁[x,y] ) :: thesis: verum

proof

take Sum (f (#) l) ; :: thesis: ( Sum (f (#) l) in the carrier of V & S₁[x, Sum (f (#) l)] )
thus ( Sum (f (#) l) in the carrier of V & S₁[x, Sum (f (#) l)] ) by C1, FIELD_7:6; :: thesis: verum

end;

end;

consider T being Function of the carrier of U, the carrier of V such that
A: for u being object st u in the carrier of U holds
S₁[u,T . u] from FUNCT_2:sch 1(AA);

now :: thesis: for u1, u2 being Element of U holds (T . u1) + (T . u2) = T . (u1 + u2)

let u1, u2 be Element of U; :: thesis: (T . u1) + (T . u2) = T . (u1 + u2)
u1 in the carrier of (Lin B) by B;
then u1 in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l1 being Linear_Combination of B1 such that
C1: u1 = Sum l1 ;
u2 in the carrier of (Lin B) by B;
then u2 in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l2 being Linear_Combination of B1 such that
C2: u2 = Sum l2 ;
reconsider l3 = l1 + l2 as Linear_Combination of B1 by VECTSP_6:24;
thus (T . u1) + (T . u2) = (Sum (f (#) l1)) + (T . (Sum l2)) by A, C1, C2
.= (Sum (f (#) l1)) + (Sum (f (#) l2)) by A
.= Sum (f (#) l3) by lemadd
.= T . (Sum (l1 + l2)) by A
.= T . (u1 + u2) by C1, C2, VECTSP_6:44 ; :: thesis: verum

end;

then C: T is additive by VECTSP_1:def 20;

now :: thesis: for a being Element of F
for u being Element of U holds a * (T . u) = T . (a * u)

let a be Element of F; :: thesis: for u being Element of U holds a * (T . u) = T . (a * u)
let u be Element of U; :: thesis: a * (T . u) = T . (a * u)
u in the carrier of (Lin B) by B;
then u in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l being Linear_Combination of B1 such that
C1: u = Sum l ;
reconsider al = a * l as Linear_Combination of B1 by VECTSP_6:31;
thus a * (T . u) = a * (Sum (f (#) l)) by A, C1
.= Sum (f (#) al) by lemmult
.= T . (Sum al) by A
.= T . (a * u) by C1, VECTSP_6:45 ; :: thesis: verum

end;

then D: T is homogeneous by MOD_2:def 2;
B c= the carrier of U ;
then B c= dom T by FUNCT_2:def 1;
then E: (dom T) /\ B = B by XBOOLE_1:28
.= dom f by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom f holds
T . x = f . x

let x be object ; :: thesis: ( x in dom f implies T . x = f . x )
assume x in dom f ; :: thesis: T . x = f . x
then reconsider w = x as Element of B ;
( w in B & B c= the carrier of U ) by H;
then w in the carrier of (Lin B) by B;
then w in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l being Linear_Combination of B1 such that
C1: w = Sum l ;
thus T . x = Sum (f (#) l) by C1, A
.= f . x by C1, lembas ; :: thesis: verum

end;

then T | B = f by E, FUNCT_1:46;
hence ex b₁ being linear-transformation of U,V st b₁ | B = f by C, D; :: thesis: verum

end;

end;