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 (lattice A),(lattice B)

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 (lattice A),(lattice B)

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 (lattice A),(lattice B) )

assume A1: ( f is one-to-one & f is additive & f is homogeneous ) ; :: thesis: FuncLatt f is Homomorphism of (lattice A),(lattice B)

for a, b being Element of (lattice A) holds

( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )

hence FuncLatt f is Homomorphism of (lattice A),(lattice B) ; :: thesis: verum

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 (lattice A),(lattice B)

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 (lattice A),(lattice B)

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 (lattice A),(lattice B) )

assume A1: ( f is one-to-one & f is additive & f is homogeneous ) ; :: thesis: FuncLatt f is Homomorphism of (lattice A),(lattice B)

for a, b being Element of (lattice A) holds

( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )

proof

then
( FuncLatt f is "\/"-preserving & FuncLatt f is "/\"-preserving )
;
let a, b be Element of (lattice A); :: thesis: ( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )

A2: (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)

hence ( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) ) by A2, LATTICE4:def 1; :: thesis: verum

end;A2: (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)

proof

FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)
by A1, Th12;
reconsider b2 = (FuncLatt f) . b as Element of (lattice B) ;

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 A3, Def7;

0. A in B1 by VECTSP_4:17;

then A5: 0. A in the carrier of B1 by STRUCT_0:def 5;

reconsider a2 = (FuncLatt f) . a as Element of (lattice B) ;

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 A6, Def7;

A10: dom f = the carrier of A by FUNCT_2:def 1;

A11: f .: the carrier of B1 is linearly-closed

then A33: f .: the carrier of B1 <> {} by A10, A5, FUNCT_1:def 6;

then consider B3 being strict Subspace of B such that

A34: the carrier of B3 = f .: the carrier of B1 by A11, VECTSP_4:34;

A35: Lin (f .: the carrier of B1) = B3 by A34, VECTSP_7:11;

ex y being Element of B st y = f . (0. A) ;

then A36: f .: the carrier of A1 <> {} by A10, A8, FUNCT_1:def 6;

then consider A3 being strict Subspace of B such that

A37: the carrier of A3 = f .: the carrier of A1 by A22, VECTSP_4:34;

reconsider AB = A3 /\ B3 as Subspace of B ;

A38: Lin (f .: the carrier of A1) = A3 by A37, VECTSP_7:11;

A39: f .: the carrier of (A1 /\ B1) is linearly-closed

then A73: P = AB by VECTSP_4:29;

(FuncLatt f) . (a "/\" b) = (FuncLatt f) . (A1 /\ B1) by A6, A3, Th8;

hence (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) by A9, A4, A7, A38, A35, A73, Th8; :: thesis: verum

end;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 A3, Def7;

0. A in B1 by VECTSP_4:17;

then A5: 0. A in the carrier of B1 by STRUCT_0:def 5;

reconsider a2 = (FuncLatt f) . a as Element of (lattice B) ;

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 A6, Def7;

A10: dom f = the carrier of A by FUNCT_2:def 1;

A11: f .: the carrier of B1 is linearly-closed

proof

A22:
f .: the carrier of A1 is linearly-closed
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

for v being Element of B st v in f .: the carrier of B1 holds

a * v in f .: the carrier of B1

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

for a being Element of F
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 A14, FUNCT_2:65;

A17: y in B1 by A15, STRUCT_0:def 5;

consider x being Element of A such that

A18: x in the carrier of B1 and

A19: v = f . x by A13, FUNCT_2:65;

x in B1 by A18, STRUCT_0:def 5;

then x + y in B1 by A17, VECTSP_4:20;

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 A1, A19, A16, VECTSP_1:def 20; :: thesis: verum

end;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 A14, FUNCT_2:65;

A17: y in B1 by A15, STRUCT_0:def 5;

consider x being Element of A such that

A18: x in the carrier of B1 and

A19: v = f . x by A13, FUNCT_2:65;

x in B1 by A18, STRUCT_0:def 5;

then x + y in B1 by A17, VECTSP_4:20;

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 A1, A19, A16, VECTSP_1:def 20; :: thesis: verum

for v being Element of B st v in f .: the carrier of B1 holds

a * v in f .: the carrier of B1

proof

hence
f .: the carrier of B1 is linearly-closed
by A12, VECTSP_4:def 1; :: thesis: verum
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 A20, STRUCT_0:def 5;

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 A1, A21, MOD_2:def 2; :: thesis: verum

end;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 A20, STRUCT_0:def 5;

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 A1, A21, MOD_2:def 2; :: thesis: verum

proof

ex y1 being Element of B st y1 = f . (0. A)
;
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

for v being Element of B st v in f .: the carrier of A1 holds

a * v in f .: the carrier of A1

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

for a being Element of F
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 A25, FUNCT_2:65;

A28: y in A1 by A26, STRUCT_0:def 5;

consider x being Element of A such that

A29: x in the carrier of A1 and

A30: v = f . x by A24, FUNCT_2:65;

x in A1 by A29, STRUCT_0:def 5;

then x + y in A1 by A28, VECTSP_4:20;

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 A1, A30, A27, VECTSP_1:def 20; :: thesis: verum

end;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 A25, FUNCT_2:65;

A28: y in A1 by A26, STRUCT_0:def 5;

consider x being Element of A such that

A29: x in the carrier of A1 and

A30: v = f . x by A24, FUNCT_2:65;

x in A1 by A29, STRUCT_0:def 5;

then x + y in A1 by A28, VECTSP_4:20;

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 A1, A30, A27, VECTSP_1:def 20; :: thesis: verum

for v being Element of B st v in f .: the carrier of A1 holds

a * v in f .: the carrier of A1

proof

hence
f .: the carrier of A1 is linearly-closed
by A23, VECTSP_4:def 1; :: thesis: verum
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 A31, STRUCT_0:def 5;

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 A1, A32, MOD_2:def 2; :: thesis: verum

end;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 A31, STRUCT_0:def 5;

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 A1, A32, MOD_2:def 2; :: thesis: verum

then A33: f .: the carrier of B1 <> {} by A10, A5, FUNCT_1:def 6;

then consider B3 being strict Subspace of B such that

A34: the carrier of B3 = f .: the carrier of B1 by A11, VECTSP_4:34;

A35: Lin (f .: the carrier of B1) = B3 by A34, VECTSP_7:11;

ex y being Element of B st y = f . (0. A) ;

then A36: f .: the carrier of A1 <> {} by A10, A8, FUNCT_1:def 6;

then consider A3 being strict Subspace of B such that

A37: the carrier of A3 = f .: the carrier of A1 by A22, VECTSP_4:34;

reconsider AB = A3 /\ B3 as Subspace of B ;

A38: Lin (f .: the carrier of A1) = A3 by A37, VECTSP_7:11;

A39: f .: the carrier of (A1 /\ B1) is linearly-closed

proof

A50:
the carrier of P c= the carrier of AB
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)

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)

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

for a being Element of F
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 A42, FUNCT_2:65;

A45: y in A1 /\ B1 by A43, STRUCT_0:def 5;

consider x being Element of A such that

A46: x in the carrier of (A1 /\ B1) and

A47: v = f . x by A41, FUNCT_2:65;

x in A1 /\ B1 by A46, STRUCT_0:def 5;

then x + y in A1 /\ B1 by A45, VECTSP_4:20;

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 A1, A47, A44, VECTSP_1:def 20; :: thesis: verum

end;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 A42, FUNCT_2:65;

A45: y in A1 /\ B1 by A43, STRUCT_0:def 5;

consider x being Element of A such that

A46: x in the carrier of (A1 /\ B1) and

A47: v = f . x by A41, FUNCT_2:65;

x in A1 /\ B1 by A46, STRUCT_0:def 5;

then x + y in A1 /\ B1 by A45, VECTSP_4:20;

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 A1, A47, A44, VECTSP_1:def 20; :: thesis: verum

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

hence
f .: the carrier of (A1 /\ B1) is linearly-closed
by A40, VECTSP_4:def 1; :: thesis: verum
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 A48, STRUCT_0:def 5;

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 A1, A49, MOD_2:def 2; :: thesis: verum

end;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 A48, STRUCT_0:def 5;

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 A1, A49, MOD_2:def 2; :: thesis: verum

proof

the carrier of AB c= the carrier of P
A51:
the carrier of (A3 /\ B3) c= f .: the carrier of (A1 /\ B1)

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)

hence x in the carrier of AB by A39, A60, Th10; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of P or x in the carrier of AB )
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 A38, VECTSP_5:3;

then x in f .: the carrier of A1 by A36, A22, Th10;

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 A36, A22, A53, Th10, FUNCT_2:65;

A56: xa in A1 by A54, STRUCT_0:def 5;

x in Lin (f .: the carrier of B1) by A35, A52, VECTSP_5:3;

then consider xa1 being Element of A such that

A57: xa1 in the carrier of B1 and

A58: x = f . xa1 by A33, A11, Th10, FUNCT_2:65;

A59: xa1 in B1 by A57, STRUCT_0:def 5;

xa1 = xa by A1, A55, A58, FUNCT_2:19;

then xa in A1 /\ B1 by A56, A59, VECTSP_5:3;

then xa in the carrier of (A1 /\ B1) by STRUCT_0:def 5;

hence x in f .: the carrier of (A1 /\ B1) by A55, FUNCT_2:35; :: thesis: verum

end;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 A38, VECTSP_5:3;

then x in f .: the carrier of A1 by A36, A22, Th10;

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 A36, A22, A53, Th10, FUNCT_2:65;

A56: xa in A1 by A54, STRUCT_0:def 5;

x in Lin (f .: the carrier of B1) by A35, A52, VECTSP_5:3;

then consider xa1 being Element of A such that

A57: xa1 in the carrier of B1 and

A58: x = f . xa1 by A33, A11, Th10, FUNCT_2:65;

A59: xa1 in B1 by A57, STRUCT_0:def 5;

xa1 = xa by A1, A55, A58, FUNCT_2:19;

then xa in A1 /\ B1 by A56, A59, VECTSP_5:3;

then xa in the carrier of (A1 /\ B1) by STRUCT_0:def 5;

hence x in f .: the carrier of (A1 /\ B1) by A55, FUNCT_2:35; :: thesis: verum

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

then
f .: the carrier of (A1 /\ B1) = the carrier of (A3 /\ B3)
by A51, XBOOLE_0:def 10;
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 A61, FUNCT_2:65;

A64: c in A1 /\ B1 by A62, STRUCT_0:def 5;

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 FUNCT_2:35, VECTSP_7:8;

c in A1 by A64, VECTSP_5:3;

then c in the carrier of A1 by STRUCT_0:def 5;

then f . c in Lin (f .: the carrier of A1) by FUNCT_2:35, VECTSP_7:8;

then x in (Lin (f .: the carrier of A1)) /\ (Lin (f .: the carrier of B1)) by A63, A65, VECTSP_5:3;

hence x in the carrier of (A3 /\ B3) by A38, A35, STRUCT_0:def 5; :: thesis: verum

end;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 A61, FUNCT_2:65;

A64: c in A1 /\ B1 by A62, STRUCT_0:def 5;

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 FUNCT_2:35, VECTSP_7:8;

c in A1 by A64, VECTSP_5:3;

then c in the carrier of A1 by STRUCT_0:def 5;

then f . c in Lin (f .: the carrier of A1) by FUNCT_2:35, VECTSP_7:8;

then x in (Lin (f .: the carrier of A1)) /\ (Lin (f .: the carrier of B1)) by A63, A65, VECTSP_5:3;

hence x in the carrier of (A3 /\ B3) by A38, A35, STRUCT_0:def 5; :: thesis: verum

hence x in the carrier of AB by A39, A60, Th10; :: thesis: verum

proof

then
the carrier of AB = the carrier of P
by A50, XBOOLE_0:def 10;
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 A35, VECTSP_5:3;

then consider xa1 being Element of A such that

A67: xa1 in the carrier of B1 and

A68: x = f . xa1 by A33, A11, Th10, FUNCT_2:65;

A69: xa1 in B1 by A67, STRUCT_0:def 5;

x in Lin (f .: the carrier of A1) by A38, A66, VECTSP_5:3;

then x in f .: the carrier of A1 by A37, A38, STRUCT_0:def 5;

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 A70, STRUCT_0:def 5;

xa1 = xa by A1, A71, A68, FUNCT_2:19;

then xa in A1 /\ B1 by A72, A69, VECTSP_5:3;

then xa in the carrier of (A1 /\ B1) by STRUCT_0:def 5;

then x in P by A71, FUNCT_2:35, VECTSP_7:8;

hence x in the carrier of P by STRUCT_0:def 5; :: thesis: verum

end;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 A35, VECTSP_5:3;

then consider xa1 being Element of A such that

A67: xa1 in the carrier of B1 and

A68: x = f . xa1 by A33, A11, Th10, FUNCT_2:65;

A69: xa1 in B1 by A67, STRUCT_0:def 5;

x in Lin (f .: the carrier of A1) by A38, A66, VECTSP_5:3;

then x in f .: the carrier of A1 by A37, A38, STRUCT_0:def 5;

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 A70, STRUCT_0:def 5;

xa1 = xa by A1, A71, A68, FUNCT_2:19;

then xa in A1 /\ B1 by A72, A69, VECTSP_5:3;

then xa in the carrier of (A1 /\ B1) by STRUCT_0:def 5;

then x in P by A71, FUNCT_2:35, VECTSP_7:8;

hence x in the carrier of P by STRUCT_0:def 5; :: thesis: verum

then A73: P = AB by VECTSP_4:29;

(FuncLatt f) . (a "/\" b) = (FuncLatt f) . (A1 /\ B1) by A6, A3, Th8;

hence (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) by A9, A4, A7, A38, A35, A73, Th8; :: thesis: verum

hence ( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) ) by A2, LATTICE4:def 1; :: thesis: verum

hence FuncLatt f is Homomorphism of (lattice A),(lattice B) ; :: thesis: verum