set M = { f where f is linear-transformation of U,V : verum } ;
set f = the linear-transformation of U,V;

now :: thesis: for o being object st o in { f where f is linear-transformation of U,V : verum } holds
o in the carrier of (Maps (U,V))

let o be object ; :: thesis: ( o in { f where f is linear-transformation of U,V : verum } implies o in the carrier of (Maps (U,V)) )
assume o in { f where f is linear-transformation of U,V : verum } ; :: thesis: o in the carrier of (Maps (U,V))
then consider g being linear-transformation of U,V such that
A: o = g ;
g in Funcs ( the carrier of U, the carrier of V) by FUNCT_2:8;
hence o in the carrier of (Maps (U,V)) by A, defmap; :: thesis: verum

end;

then { f where f is linear-transformation of U,V : verum } c= the carrier of (Maps (U,V)) ;
then reconsider M = { f where f is linear-transformation of U,V : verum } as Subset of (Maps (U,V)) ;
A: the linear-transformation of U,V in M ;

B: now :: thesis: for v, u being Element of (Maps (U,V)) st v in M & u in M holds
v + u in M

let v, u be Element of (Maps (U,V)); :: thesis: ( v in M & u in M implies v + u in M )
assume B0: ( v in M & u in M ) ; :: thesis: v + u in M
then consider g1 being linear-transformation of U,V such that
B1: v = g1 ;
consider g2 being linear-transformation of U,V such that
B2: u = g2 by B0;
B3: g1 '+' g2 is linear-transformation of U,V by LT1;
v + u = (mapAdd ( the carrier of U,V)) . (g1,g2) by B1, B2, defmap
.= g1 '+' g2 by dA ;
hence v + u in M by B3; :: thesis: verum

end;

now :: thesis: for a being Element of F
for v being Element of (Maps (U,V)) st v in M holds
a * v in M

let a be Element of F; :: thesis: for v being Element of (Maps (U,V)) st v in M holds
a * v in M
let v be Element of (Maps (U,V)); :: thesis: ( v in M implies a * v in M )
assume v in M ; :: thesis: a * v in M
then consider g1 being linear-transformation of U,V such that
C1: v = g1 ;
C2: a '*' g1 is linear-transformation of U,V by LT2;
a * v = the lmult of (Maps ( the carrier of U,V)) . (a,v) by VECTSP_1:def 12
.= (mapMult ( the carrier of U,V)) . (a,g1) by C1, defmap
.= a '*' g1 by dM ;
hence a * v in M by C2; :: thesis: verum

end;

hence ex b₁ being strict Subspace of Maps (U,V) st the carrier of b₁ = { f where f is linear-transformation of U,V : verum } by A, B, VECTSP_4:def 1, VECTSP_4:34; :: thesis: verum