defpred S_{1}[ 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_{1}[x,y] )

A4: for x being object st x in the carrier of (lattice A) holds

S_{1}[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

$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

proof

consider f1 being Function of the carrier of (lattice A), the carrier of (lattice B) such that
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_{1}[x,y] ) )

assume x in the carrier of (lattice A) ; :: thesis: ex y being object st

( y in the carrier of (lattice B) & S_{1}[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_{1}[x,Y] )

thus ( Y in the carrier of (lattice B) & S_{1}[x,Y] )
by A2, A3, VECTSP_5:def 3; :: thesis: verum

end;( y in the carrier of (lattice B) & S

assume x in the carrier of (lattice A) ; :: thesis: ex y being object st

( y in the carrier of (lattice B) & S

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

thus ( Y in the carrier of (lattice B) & S

A4: for x being object st x in the carrier of (lattice A) holds

S

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;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