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

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

let f be Function of A,B; :: thesis: ( f is one-to-one & f is additive & f is homogeneous implies FuncLatt f is Homomorphism of (),() )
assume A1: ( f is one-to-one & f is additive & f is homogeneous ) ; :: thesis: FuncLatt f is Homomorphism of (),()
for a, b being Element of () holds
( () . (a "\/" b) = (() . a) "\/" (() . b) & () . (a "/\" b) = (() . a) "/\" (() . b) )
proof
let a, b be Element of (); :: thesis: ( () . (a "\/" b) = (() . a) "\/" (() . b) & () . (a "/\" b) = (() . a) "/\" (() . b) )
A2: (FuncLatt f) . (a "/\" b) = (() . a) "/\" (() . b)
proof
reconsider b2 = () . b as Element of () ;
consider B1 being strict Subspace of A such that
A3: B1 = b by VECTSP_5:def 3;
A4: b2 = Lin (f .: the carrier of B1) by ;
0. A in B1 by VECTSP_4:17;
then A5: 0. A in the carrier of B1 by STRUCT_0:def 5;
reconsider a2 = () . a as Element of () ;
consider A1 being strict Subspace of A such that
A6: A1 = a by VECTSP_5:def 3;
reconsider P = Lin (f .: the carrier of (A1 /\ B1)) as Subspace of B ;
A7: (FuncLatt f) . (A1 /\ B1) = Lin (f .: the carrier of (A1 /\ B1)) by Def7;
0. A in A1 by VECTSP_4:17;
then A8: 0. A in the carrier of A1 by STRUCT_0:def 5;
A9: a2 = Lin (f .: the carrier of A1) by ;
A10: dom f = the carrier of A by FUNCT_2:def 1;
A11: f .: the carrier of B1 is linearly-closed
proof
set BB = f .: the carrier of B1;
A12: for v, u being Element of B st v in f .: the carrier of B1 & u in f .: the carrier of B1 holds
v + u in f .: the carrier of B1
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of B1 & u in f .: the carrier of B1 implies v + u in f .: the carrier of B1 )
assume that
A13: v in f .: the carrier of B1 and
A14: u in f .: the carrier of B1 ; :: thesis: v + u in f .: the carrier of B1
consider y being Element of A such that
A15: y in the carrier of B1 and
A16: u = f . y by ;
A17: y in B1 by ;
consider x being Element of A such that
A18: x in the carrier of B1 and
A19: v = f . x by ;
x in B1 by ;
then x + y in B1 by ;
then x + y in the carrier of B1 by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of B1 by FUNCT_2:35;
hence v + u in f .: the carrier of B1 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1

let v be Element of B; :: thesis: ( v in f .: the carrier of B1 implies a * v in f .: the carrier of B1 )
assume v in f .: the carrier of B1 ; :: thesis: a * v in f .: the carrier of B1
then consider x being Element of A such that
A20: x in the carrier of B1 and
A21: v = f . x by FUNCT_2:65;
x in B1 by ;
then a * x in B1 by VECTSP_4:21;
then a * x in the carrier of B1 by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of B1 by FUNCT_2:35;
hence a * v in f .: the carrier of B1 by ; :: thesis: verum
end;
hence f .: the carrier of B1 is linearly-closed by ; :: thesis: verum
end;
A22: f .: the carrier of A1 is linearly-closed
proof
set BB = f .: the carrier of A1;
A23: for v, u being Element of B st v in f .: the carrier of A1 & u in f .: the carrier of A1 holds
v + u in f .: the carrier of A1
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of A1 & u in f .: the carrier of A1 implies v + u in f .: the carrier of A1 )
assume that
A24: v in f .: the carrier of A1 and
A25: u in f .: the carrier of A1 ; :: thesis: v + u in f .: the carrier of A1
consider y being Element of A such that
A26: y in the carrier of A1 and
A27: u = f . y by ;
A28: y in A1 by ;
consider x being Element of A such that
A29: x in the carrier of A1 and
A30: v = f . x by ;
x in A1 by ;
then x + y in A1 by ;
then x + y in the carrier of A1 by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of A1 by FUNCT_2:35;
hence v + u in f .: the carrier of A1 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1

let v be Element of B; :: thesis: ( v in f .: the carrier of A1 implies a * v in f .: the carrier of A1 )
assume v in f .: the carrier of A1 ; :: thesis: a * v in f .: the carrier of A1
then consider x being Element of A such that
A31: x in the carrier of A1 and
A32: v = f . x by FUNCT_2:65;
x in A1 by ;
then a * x in A1 by VECTSP_4:21;
then a * x in the carrier of A1 by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of A1 by FUNCT_2:35;
hence a * v in f .: the carrier of A1 by ; :: thesis: verum
end;
hence f .: the carrier of A1 is linearly-closed by ; :: thesis: verum
end;
ex y1 being Element of B st y1 = f . (0. A) ;
then A33: f .: the carrier of B1 <> {} by ;
then consider B3 being strict Subspace of B such that
A34: the carrier of B3 = f .: the carrier of B1 by ;
A35: Lin (f .: the carrier of B1) = B3 by ;
ex y being Element of B st y = f . (0. A) ;
then A36: f .: the carrier of A1 <> {} by ;
then consider A3 being strict Subspace of B such that
A37: the carrier of A3 = f .: the carrier of A1 by ;
reconsider AB = A3 /\ B3 as Subspace of B ;
A38: Lin (f .: the carrier of A1) = A3 by ;
A39: f .: the carrier of (A1 /\ B1) is linearly-closed
proof
set BB = f .: the carrier of (A1 /\ B1);
A40: for v, u being Element of B st v in f .: the carrier of (A1 /\ B1) & u in f .: the carrier of (A1 /\ B1) holds
v + u in f .: the carrier of (A1 /\ B1)
proof
let v, u be Element of B; :: thesis: ( v in f .: the carrier of (A1 /\ B1) & u in f .: the carrier of (A1 /\ B1) implies v + u in f .: the carrier of (A1 /\ B1) )
assume that
A41: v in f .: the carrier of (A1 /\ B1) and
A42: u in f .: the carrier of (A1 /\ B1) ; :: thesis: v + u in f .: the carrier of (A1 /\ B1)
consider y being Element of A such that
A43: y in the carrier of (A1 /\ B1) and
A44: u = f . y by ;
A45: y in A1 /\ B1 by ;
consider x being Element of A such that
A46: x in the carrier of (A1 /\ B1) and
A47: v = f . x by ;
x in A1 /\ B1 by ;
then x + y in A1 /\ B1 by ;
then x + y in the carrier of (A1 /\ B1) by STRUCT_0:def 5;
then f . (x + y) in f .: the carrier of (A1 /\ B1) by FUNCT_2:35;
hence v + u in f .: the carrier of (A1 /\ B1) by ; :: thesis: verum
end;
for a being Element of F
for v being Element of B st v in f .: the carrier of (A1 /\ B1) holds
a * v in f .: the carrier of (A1 /\ B1)
proof
let a be Element of F; :: thesis: for v being Element of B st v in f .: the carrier of (A1 /\ B1) holds
a * v in f .: the carrier of (A1 /\ B1)

let v be Element of B; :: thesis: ( v in f .: the carrier of (A1 /\ B1) implies a * v in f .: the carrier of (A1 /\ B1) )
assume v in f .: the carrier of (A1 /\ B1) ; :: thesis: a * v in f .: the carrier of (A1 /\ B1)
then consider x being Element of A such that
A48: x in the carrier of (A1 /\ B1) and
A49: v = f . x by FUNCT_2:65;
x in A1 /\ B1 by ;
then a * x in A1 /\ B1 by VECTSP_4:21;
then a * x in the carrier of (A1 /\ B1) by STRUCT_0:def 5;
then f . (a * x) in f .: the carrier of (A1 /\ B1) by FUNCT_2:35;
hence a * v in f .: the carrier of (A1 /\ B1) by ; :: thesis: verum
end;
hence f .: the carrier of (A1 /\ B1) is linearly-closed by ; :: thesis: verum
end;
A50: the carrier of P c= the carrier of AB
proof
A51: the carrier of (A3 /\ B3) c= f .: the carrier of (A1 /\ B1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (A3 /\ B3) or x in f .: the carrier of (A1 /\ B1) )
assume x in the carrier of (A3 /\ B3) ; :: thesis: x in f .: the carrier of (A1 /\ B1)
then A52: x in A3 /\ B3 by STRUCT_0:def 5;
then A53: x in Lin (f .: the carrier of A1) by ;
then x in f .: the carrier of A1 by ;
then reconsider x = x as Element of B ;
consider xa being Element of A such that
A54: xa in the carrier of A1 and
A55: x = f . xa by ;
A56: xa in A1 by ;
x in Lin (f .: the carrier of B1) by ;
then consider xa1 being Element of A such that
A57: xa1 in the carrier of B1 and
A58: x = f . xa1 by ;
A59: xa1 in B1 by ;
xa1 = xa by ;
then xa in A1 /\ B1 by ;
then xa in the carrier of (A1 /\ B1) by STRUCT_0:def 5;
hence x in f .: the carrier of (A1 /\ B1) by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of P or x in the carrier of AB )
assume x in the carrier of P ; :: thesis: x in the carrier of AB
then A60: x in P by STRUCT_0:def 5;
f .: the carrier of (A1 /\ B1) c= the carrier of (A3 /\ B3)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: the carrier of (A1 /\ B1) or x in the carrier of (A3 /\ B3) )
assume A61: x in f .: the carrier of (A1 /\ B1) ; :: thesis: x in the carrier of (A3 /\ B3)
then reconsider x = x as Element of B ;
consider c being Element of A such that
A62: c in the carrier of (A1 /\ B1) and
A63: x = f . c by ;
A64: c in A1 /\ B1 by ;
then c in B1 by VECTSP_5:3;
then c in the carrier of B1 by STRUCT_0:def 5;
then A65: f . c in Lin (f .: the carrier of B1) by ;
c in A1 by ;
then c in the carrier of A1 by STRUCT_0:def 5;
then f . c in Lin (f .: the carrier of A1) by ;
then x in (Lin (f .: the carrier of A1)) /\ (Lin (f .: the carrier of B1)) by ;
hence x in the carrier of (A3 /\ B3) by ; :: thesis: verum
end;
then f .: the carrier of (A1 /\ B1) = the carrier of (A3 /\ B3) by ;
hence x in the carrier of AB by ; :: thesis: verum
end;
the carrier of AB c= the carrier of P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of AB or x in the carrier of P )
assume x in the carrier of AB ; :: thesis: x in the carrier of P
then A66: x in A3 /\ B3 by STRUCT_0:def 5;
then x in Lin (f .: the carrier of B1) by ;
then consider xa1 being Element of A such that
A67: xa1 in the carrier of B1 and
A68: x = f . xa1 by ;
A69: xa1 in B1 by ;
x in Lin (f .: the carrier of A1) by ;
then x in f .: the carrier of A1 by ;
then consider xa being Element of A such that
A70: xa in the carrier of A1 and
A71: x = f . xa by FUNCT_2:65;
A72: xa in A1 by ;
xa1 = xa by ;
then xa in A1 /\ B1 by ;
then xa in the carrier of (A1 /\ B1) by STRUCT_0:def 5;
then x in P by ;
hence x in the carrier of P by STRUCT_0:def 5; :: thesis: verum
end;
then the carrier of AB = the carrier of P by ;
then A73: P = AB by VECTSP_4:29;
(FuncLatt f) . (a "/\" b) = () . (A1 /\ B1) by A6, A3, Th8;
hence (FuncLatt f) . (a "/\" b) = (() . a) "/\" (() . b) by A9, A4, A7, A38, A35, A73, Th8; :: thesis: verum
end;
FuncLatt f is sup-Semilattice-Homomorphism of (),() by ;
hence ( (FuncLatt f) . (a "\/" b) = (() . a) "\/" (() . b) & () . (a "/\" b) = (() . a) "/\" (() . b) ) by ; :: thesis: verum
end;
then ( FuncLatt f is "\/"-preserving & FuncLatt f is "/\"-preserving ) ;
hence FuncLatt f is Homomorphism of (),() ; :: thesis: verum