defpred S1[ object , object ] means for S being Subspace of A st S = \$1 holds
\$2 = Lin (f .: the carrier of S);
A1: for x being object st x in the carrier of () holds
ex y being object st
( y in the carrier of () & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of () implies ex y being object st
( y in the carrier of () & S1[x,y] ) )

assume x in the carrier of () ; :: thesis: ex y being object st
( y in the carrier of () & S1[x,y] )

then consider X being strict Subspace of A such that
A2: X = x by VECTSP_5:def 3;
reconsider y = f .: the carrier of X as Subset of B ;
consider Y being strict Subspace of B such that
A3: Y = Lin y ;
take Y ; :: thesis: ( Y in the carrier of () & S1[x,Y] )
thus ( Y in the carrier of () & S1[x,Y] ) by ; :: thesis: verum
end;
consider f1 being Function of the carrier of (), the carrier of () such that
A4: for x being object st x in the carrier of () holds
S1[x,f1 . x] from take f1 ; :: thesis: for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
f1 . S = Lin B0

thus for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
f1 . S = Lin B0 :: thesis: verum
proof
let S be strict Subspace of A; :: thesis: for B0 being Subset of B st B0 = f .: the carrier of S holds
f1 . S = Lin B0

let B0 be Subset of B; :: thesis: ( B0 = f .: the carrier of S implies f1 . S = Lin B0 )
A5: S is Element of Subspaces A by VECTSP_5:def 3;
assume B0 = f .: the carrier of S ; :: thesis: f1 . S = Lin B0
hence f1 . S = Lin B0 by A4, A5; :: thesis: verum
end;