let F be Field; :: thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one

let A, B be strict VectSp of F; :: thesis: for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one

let f be Function of A,B; :: thesis: ( f is additive & f is homogeneous & f is one-to-one implies FuncLatt f is one-to-one )
assume that
A1: ( f is additive & f is homogeneous ) and
A2: f is one-to-one ; :: thesis:
for x1, x2 being object st x1 in dom () & x2 in dom () & () . x1 = () . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom () & x2 in dom () & () . x1 = () . x2 implies x1 = x2 )
assume that
A3: x1 in dom () and
A4: x2 in dom () and
A5: (FuncLatt f) . x1 = () . x2 ; :: thesis: x1 = x2
consider X1 being strict Subspace of A such that
A6: X1 = x1 by ;
A7: f .: the carrier of X1 is linearly-closed
proof
set BB = f .: the carrier of X1;
A8: for v, u being Element of B st v in f .: the carrier of X1 & u in f .: the carrier of X1 holds
v + u in f .: the carrier of X1
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of X1 & u in f .: the carrier of X1 implies v + u in f .: the carrier of X1 )
assume that
A9: v in f .: the carrier of X1 and
A10: u in f .: the carrier of X1 ; :: thesis: v + u in f .: the carrier of X1
consider y being Element of A such that
A11: y in the carrier of X1 and
A12: u = f . y by ;
A13: y in X1 by ;
consider x being Element of A such that
A14: x in the carrier of X1 and
A15: v = f . x by ;
x in X1 by ;
then x + y in X1 by ;
then x + y in the carrier of X1 by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of X1 by FUNCT_2:35;
hence v + u in f .: the carrier of X1 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of X1 holds
a * v in f .: the carrier of X1
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of X1 holds
a * v in f .: the carrier of X1

let v be Element of B; :: thesis: ( v in f .: the carrier of X1 implies a * v in f .: the carrier of X1 )
assume v in f .: the carrier of X1 ; :: thesis: a * v in f .: the carrier of X1
then consider x being Element of A such that
A16: x in the carrier of X1 and
A17: v = f . x by FUNCT_2:65;
x in X1 by ;
then a * x in X1 by VECTSP_4:21;
then a * x in the carrier of X1 by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of X1 by FUNCT_2:35;
hence a * v in f .: the carrier of X1 by ; :: thesis: verum
end;
hence f .: the carrier of X1 is linearly-closed by ; :: thesis: verum
end;
consider A1 being Subset of B such that
A18: A1 = f .: the carrier of X1 ;
0. A in X1 by VECTSP_4:17;
then A19: 0. A in the carrier of X1 by STRUCT_0:def 5;
A20: dom f = the carrier of A by FUNCT_2:def 1;
ex y being Element of B st y = f . (0. A) ;
then f .: the carrier of X1 <> {} by ;
then A21: ex B1 being strict Subspace of B st the carrier of B1 = f .: the carrier of X1 by ;
A22: (FuncLatt f) . X1 = Lin A1 by ;
consider X2 being strict Subspace of A such that
A23: X2 = x2 by ;
A24: f .: the carrier of X2 is linearly-closed
proof
set BB = f .: the carrier of X2;
A25: for v, u being Element of B st v in f .: the carrier of X2 & u in f .: the carrier of X2 holds
v + u in f .: the carrier of X2
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of X2 & u in f .: the carrier of X2 implies v + u in f .: the carrier of X2 )
assume that
A26: v in f .: the carrier of X2 and
A27: u in f .: the carrier of X2 ; :: thesis: v + u in f .: the carrier of X2
consider y being Element of A such that
A28: y in the carrier of X2 and
A29: u = f . y by ;
A30: y in X2 by ;
consider x being Element of A such that
A31: x in the carrier of X2 and
A32: v = f . x by ;
x in X2 by ;
then x + y in X2 by ;
then x + y in the carrier of X2 by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of X2 by FUNCT_2:35;
hence v + u in f .: the carrier of X2 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of X2 holds
a * v in f .: the carrier of X2
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of X2 holds
a * v in f .: the carrier of X2

let v be Element of B; :: thesis: ( v in f .: the carrier of X2 implies a * v in f .: the carrier of X2 )
assume v in f .: the carrier of X2 ; :: thesis: a * v in f .: the carrier of X2
then consider x being Element of A such that
A33: x in the carrier of X2 and
A34: v = f . x by FUNCT_2:65;
x in X2 by ;
then a * x in X2 by VECTSP_4:21;
then a * x in the carrier of X2 by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of X2 by FUNCT_2:35;
hence a * v in f .: the carrier of X2 by ; :: thesis: verum
end;
hence f .: the carrier of X2 is linearly-closed by ; :: thesis: verum
end;
consider A2 being Subset of B such that
A35: A2 = f .: the carrier of X2 ;
A36: (FuncLatt f) . X2 = Lin A2 by ;
0. A in X2 by VECTSP_4:17;
then A37: 0. A in the carrier of X2 by STRUCT_0:def 5;
ex y being Element of B st y = f . (0. A) ;
then f .: the carrier of X2 <> {} by ;
then consider B2 being strict Subspace of B such that
A38: the carrier of B2 = f .: the carrier of X2 by ;
Lin (f .: the carrier of X2) = B2 by ;
then A39: f .: the carrier of X1 = f .: the carrier of X2 by A5, A6, A23, A18, A35, A22, A36, A21, A38, VECTSP_7:11;
the carrier of X2 c= dom f by ;
then A40: the carrier of X2 c= the carrier of X1 by ;
the carrier of X1 c= dom f by ;
then the carrier of X1 c= the carrier of X2 by ;
then the carrier of X1 = the carrier of X2 by ;
hence x1 = x2 by ; :: thesis: verum
end;
hence FuncLatt f is one-to-one by FUNCT_1:def 4; :: thesis: verum