defpred S₁[ 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 (lattice A) holds
ex y being object st
( y in the carrier of (lattice B) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (lattice A) implies ex y being object st
( y in the carrier of (lattice B) & S₁[x,y] ) )
assume x in the carrier of (lattice A) ; :: thesis: ex y being object st
( y in the carrier of (lattice B) & S₁[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 (lattice B) & S₁[x,Y] )
thus ( Y in the carrier of (lattice B) & S₁[x,Y] ) by A2, A3, VECTSP_5:def 3; :: thesis: verum

end;

consider f1 being Function of the carrier of (lattice A), the carrier of (lattice B) such that
A4: for x being object st x in the carrier of (lattice A) holds
S₁[x,f1 . x] from FUNCT_2:sch 1(A1);
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;