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 holds

FuncLatt f is sup-Semilattice-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 additive & f is homogeneous holds

FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)

let f be Function of A,B; :: thesis: ( f is additive & f is homogeneous implies FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B) )

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

FuncLatt f is "\/"-preserving

for f being Function of A,B st f is additive & f is homogeneous holds

FuncLatt f is sup-Semilattice-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 additive & f is homogeneous holds

FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)

let f be Function of A,B; :: thesis: ( f is additive & f is homogeneous implies FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B) )

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

FuncLatt f is "\/"-preserving

proof

hence
FuncLatt f is sup-Semilattice-Homomorphism of (lattice A),(lattice B)
; :: thesis: verum
let a, b be Element of (lattice A); :: according to LATTICE4:def 1 :: thesis: (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)

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

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

proof

hence
(FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
; :: thesis: verum
reconsider b2 = (FuncLatt f) . b as Element of (lattice B) ;

consider B1 being strict Subspace of A such that

A2: B1 = b by VECTSP_5:def 3;

A3: b2 = Lin (f .: the carrier of B1) by A2, Def7;

0. A in B1 by VECTSP_4:17;

then A4: 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

A5: A1 = a by VECTSP_5:def 3;

A6: f .: the carrier of A1 is linearly-closed

A28: (FuncLatt f) . (A1 + B1) = Lin (f .: the carrier of (A1 + B1)) by Def7;

0. A in A1 by VECTSP_4:17;

then A29: 0. A in the carrier of A1 by STRUCT_0:def 5;

A30: a2 = Lin (f .: the carrier of A1) by A5, Def7;

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

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

then A32: f .: the carrier of B1 <> {} by A31, A4, FUNCT_1:def 6;

then consider B3 being strict Subspace of B such that

A33: the carrier of B3 = f .: the carrier of B1 by A17, VECTSP_4:34;

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

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

then A35: f .: the carrier of A1 <> {} by A31, A29, FUNCT_1:def 6;

then consider A3 being strict Subspace of B such that

A36: the carrier of A3 = f .: the carrier of A1 by A6, VECTSP_4:34;

reconsider AB = A3 + B3 as Subspace of B ;

A37: the carrier of AB c= the carrier of P

A53: f .: the carrier of (A1 + B1) is linearly-closed

then A82: P = AB by VECTSP_4:29;

(FuncLatt f) . (a "\/" b) = (FuncLatt f) . (A1 + B1) by A5, A2, Th7;

hence (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) by A30, A3, A28, A52, A34, A82, Th7; :: thesis: verum

end;consider B1 being strict Subspace of A such that

A2: B1 = b by VECTSP_5:def 3;

A3: b2 = Lin (f .: the carrier of B1) by A2, Def7;

0. A in B1 by VECTSP_4:17;

then A4: 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

A5: A1 = a by VECTSP_5:def 3;

A6: f .: the carrier of A1 is linearly-closed

proof

A17:
f .: the carrier of B1 is linearly-closed
set BB = f .: the carrier of A1;

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

A8: v in f .: the carrier of A1 and

A9: u in f .: the carrier of A1 ; :: thesis: v + u in f .: the carrier of A1

consider y being Element of A such that

A10: y in the carrier of A1 and

A11: u = f . y by A9, FUNCT_2:65;

A12: y in A1 by A10, STRUCT_0:def 5;

consider x being Element of A such that

A13: x in the carrier of A1 and

A14: v = f . x by A8, FUNCT_2:65;

x in A1 by A13, STRUCT_0:def 5;

then x + y in A1 by A12, 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, A14, A11, VECTSP_1:def 20; :: thesis: verum

end;assume that

A8: v in f .: the carrier of A1 and

A9: u in f .: the carrier of A1 ; :: thesis: v + u in f .: the carrier of A1

consider y being Element of A such that

A10: y in the carrier of A1 and

A11: u = f . y by A9, FUNCT_2:65;

A12: y in A1 by A10, STRUCT_0:def 5;

consider x being Element of A such that

A13: x in the carrier of A1 and

A14: v = f . x by A8, FUNCT_2:65;

x in A1 by A13, STRUCT_0:def 5;

then x + y in A1 by A12, 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, A14, A11, 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 A7, 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

A15: x in the carrier of A1 and

A16: v = f . x by FUNCT_2:65;

x in A1 by A15, 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, A16, 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

A15: x in the carrier of A1 and

A16: v = f . x by FUNCT_2:65;

x in A1 by A15, 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, A16, MOD_2:def 2; :: thesis: verum

proof

reconsider P = Lin (f .: the carrier of (A1 + B1)) as Subspace of B ;
set BB = f .: the carrier of B1;

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

A19: v in f .: the carrier of B1 and

A20: u in f .: the carrier of B1 ; :: thesis: v + u in f .: the carrier of B1

consider y being Element of A such that

A21: y in the carrier of B1 and

A22: u = f . y by A20, FUNCT_2:65;

A23: y in B1 by A21, STRUCT_0:def 5;

consider x being Element of A such that

A24: x in the carrier of B1 and

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

x in B1 by A24, STRUCT_0:def 5;

then x + y in B1 by A23, 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, A25, A22, VECTSP_1:def 20; :: thesis: verum

end;assume that

A19: v in f .: the carrier of B1 and

A20: u in f .: the carrier of B1 ; :: thesis: v + u in f .: the carrier of B1

consider y being Element of A such that

A21: y in the carrier of B1 and

A22: u = f . y by A20, FUNCT_2:65;

A23: y in B1 by A21, STRUCT_0:def 5;

consider x being Element of A such that

A24: x in the carrier of B1 and

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

x in B1 by A24, STRUCT_0:def 5;

then x + y in B1 by A23, 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, A25, A22, 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 A18, 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

A26: x in the carrier of B1 and

A27: v = f . x by FUNCT_2:65;

x in B1 by A26, 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, A27, 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

A26: x in the carrier of B1 and

A27: v = f . x by FUNCT_2:65;

x in B1 by A26, 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, A27, MOD_2:def 2; :: thesis: verum

A28: (FuncLatt f) . (A1 + B1) = Lin (f .: the carrier of (A1 + B1)) by Def7;

0. A in A1 by VECTSP_4:17;

then A29: 0. A in the carrier of A1 by STRUCT_0:def 5;

A30: a2 = Lin (f .: the carrier of A1) by A5, Def7;

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

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

then A32: f .: the carrier of B1 <> {} by A31, A4, FUNCT_1:def 6;

then consider B3 being strict Subspace of B such that

A33: the carrier of B3 = f .: the carrier of B1 by A17, VECTSP_4:34;

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

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

then A35: f .: the carrier of A1 <> {} by A31, A29, FUNCT_1:def 6;

then consider A3 being strict Subspace of B such that

A36: the carrier of A3 = f .: the carrier of A1 by A6, VECTSP_4:34;

reconsider AB = A3 + B3 as Subspace of B ;

A37: the carrier of AB c= the carrier of P

proof

A52:
Lin (f .: the carrier of A1) = A3
by A36, VECTSP_7:11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of AB or x in the carrier of P )

A38: f .: the carrier of A1 c= f .: the carrier of (A1 + B1)

then x in A3 + B3 by STRUCT_0:def 5;

then consider u, v being Element of B such that

A48: u in A3 and

A49: v in B3 and

A50: x = u + v by VECTSP_5:1;

v in f .: the carrier of B1 by A33, A49, STRUCT_0:def 5;

then A51: v in P by A43, VECTSP_7:8;

u in f .: the carrier of A1 by A36, A48, STRUCT_0:def 5;

then u in P by A38, VECTSP_7:8;

then x in P by A50, A51, VECTSP_4:20;

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

end;A38: f .: the carrier of A1 c= f .: the carrier of (A1 + B1)

proof

A43:
f .: the carrier of B1 c= f .: the carrier of (A1 + B1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: the carrier of A1 or x in f .: the carrier of (A1 + B1) )

A39: the carrier of A1 c= the carrier of (A1 + B1)

then reconsider x = x as Element of B ;

ex c being Element of A st

( c in the carrier of A1 & x = f . c ) by A42, FUNCT_2:65;

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

end;A39: the carrier of A1 c= the carrier of (A1 + B1)

proof

assume A42:
x in f .: the carrier of A1
; :: thesis: x in f .: the carrier of (A1 + B1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A1 or x in the carrier of (A1 + B1) )

assume A40: x in the carrier of A1 ; :: thesis: x in the carrier of (A1 + B1)

then A41: x in A1 by STRUCT_0:def 5;

the carrier of A1 c= the carrier of A by VECTSP_4:def 2;

then reconsider x = x as Element of A by A40;

x in A1 + B1 by A41, VECTSP_5:2;

hence x in the carrier of (A1 + B1) by STRUCT_0:def 5; :: thesis: verum

end;assume A40: x in the carrier of A1 ; :: thesis: x in the carrier of (A1 + B1)

then A41: x in A1 by STRUCT_0:def 5;

the carrier of A1 c= the carrier of A by VECTSP_4:def 2;

then reconsider x = x as Element of A by A40;

x in A1 + B1 by A41, VECTSP_5:2;

hence x in the carrier of (A1 + B1) by STRUCT_0:def 5; :: thesis: verum

then reconsider x = x as Element of B ;

ex c being Element of A st

( c in the carrier of A1 & x = f . c ) by A42, FUNCT_2:65;

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

proof

assume
x in the carrier of AB
; :: thesis: x in the carrier of P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: the carrier of B1 or x in f .: the carrier of (A1 + B1) )

A44: the carrier of B1 c= the carrier of (A1 + B1)

then reconsider x = x as Element of B ;

ex c being Element of A st

( c in the carrier of B1 & x = f . c ) by A47, FUNCT_2:65;

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

end;A44: the carrier of B1 c= the carrier of (A1 + B1)

proof

assume A47:
x in f .: the carrier of B1
; :: thesis: x in f .: the carrier of (A1 + B1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of B1 or x in the carrier of (A1 + B1) )

assume A45: x in the carrier of B1 ; :: thesis: x in the carrier of (A1 + B1)

then A46: x in B1 by STRUCT_0:def 5;

the carrier of B1 c= the carrier of A by VECTSP_4:def 2;

then reconsider x = x as Element of A by A45;

x in A1 + B1 by A46, VECTSP_5:2;

hence x in the carrier of (A1 + B1) by STRUCT_0:def 5; :: thesis: verum

end;assume A45: x in the carrier of B1 ; :: thesis: x in the carrier of (A1 + B1)

then A46: x in B1 by STRUCT_0:def 5;

the carrier of B1 c= the carrier of A by VECTSP_4:def 2;

then reconsider x = x as Element of A by A45;

x in A1 + B1 by A46, VECTSP_5:2;

hence x in the carrier of (A1 + B1) by STRUCT_0:def 5; :: thesis: verum

then reconsider x = x as Element of B ;

ex c being Element of A st

( c in the carrier of B1 & x = f . c ) by A47, FUNCT_2:65;

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

then x in A3 + B3 by STRUCT_0:def 5;

then consider u, v being Element of B such that

A48: u in A3 and

A49: v in B3 and

A50: x = u + v by VECTSP_5:1;

v in f .: the carrier of B1 by A33, A49, STRUCT_0:def 5;

then A51: v in P by A43, VECTSP_7:8;

u in f .: the carrier of A1 by A36, A48, STRUCT_0:def 5;

then u in P by A38, VECTSP_7:8;

then x in P by A50, A51, VECTSP_4:20;

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

A53: f .: the carrier of (A1 + B1) is linearly-closed

proof

the carrier of P c= the carrier of AB
set BB = f .: the carrier of (A1 + B1);

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

A55: v in f .: the carrier of (A1 + B1) and

A56: 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

A57: y in the carrier of (A1 + B1) and

A58: u = f . y by A56, FUNCT_2:65;

A59: y in A1 + B1 by A57, STRUCT_0:def 5;

consider x being Element of A such that

A60: x in the carrier of (A1 + B1) and

A61: v = f . x by A55, FUNCT_2:65;

x in A1 + B1 by A60, STRUCT_0:def 5;

then x + y in A1 + B1 by A59, 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, A61, A58, VECTSP_1:def 20; :: thesis: verum

end;assume that

A55: v in f .: the carrier of (A1 + B1) and

A56: 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

A57: y in the carrier of (A1 + B1) and

A58: u = f . y by A56, FUNCT_2:65;

A59: y in A1 + B1 by A57, STRUCT_0:def 5;

consider x being Element of A such that

A60: x in the carrier of (A1 + B1) and

A61: v = f . x by A55, FUNCT_2:65;

x in A1 + B1 by A60, STRUCT_0:def 5;

then x + y in A1 + B1 by A59, 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, A61, A58, 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 A54, 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

A62: x in the carrier of (A1 + B1) and

A63: v = f . x by FUNCT_2:65;

x in A1 + B1 by A62, 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, A63, 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

A62: x in the carrier of (A1 + B1) and

A63: v = f . x by FUNCT_2:65;

x in A1 + B1 by A62, 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, A63, MOD_2:def 2; :: thesis: verum

proof

then
the carrier of AB = the carrier of P
by A37, XBOOLE_0:def 10;
A64:
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 A73: 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 A53, A73, 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 x in A3 + B3 by STRUCT_0:def 5;

then consider vb, ub being Element of B such that

A65: vb in A3 and

A66: ub in B3 and

A67: x = vb + ub by VECTSP_5:1;

consider ua being Element of A such that

A68: ua in the carrier of B1 and

A69: ub = f . ua by A32, A17, A34, A66, Th10, FUNCT_2:65;

ua in B1 by A68, STRUCT_0:def 5;

then A70: ua in A1 + B1 by VECTSP_5:2;

consider va being Element of A such that

A71: va in the carrier of A1 and

A72: vb = f . va by A35, A6, A52, A65, Th10, FUNCT_2:65;

va in A1 by A71, STRUCT_0:def 5;

then va in A1 + B1 by VECTSP_5:2;

then ua + va in A1 + B1 by A70, VECTSP_4:20;

then ua + va in the carrier of (A1 + B1) by STRUCT_0:def 5;

then f . (ua + va) in f .: the carrier of (A1 + B1) by FUNCT_2:35;

hence x in f .: the carrier of (A1 + B1) by A1, A67, A72, A69, VECTSP_1:def 20; :: thesis: verum

end;assume x in the carrier of (A3 + B3) ; :: thesis: x in f .: the carrier of (A1 + B1)

then x in A3 + B3 by STRUCT_0:def 5;

then consider vb, ub being Element of B such that

A65: vb in A3 and

A66: ub in B3 and

A67: x = vb + ub by VECTSP_5:1;

consider ua being Element of A such that

A68: ua in the carrier of B1 and

A69: ub = f . ua by A32, A17, A34, A66, Th10, FUNCT_2:65;

ua in B1 by A68, STRUCT_0:def 5;

then A70: ua in A1 + B1 by VECTSP_5:2;

consider va being Element of A such that

A71: va in the carrier of A1 and

A72: vb = f . va by A35, A6, A52, A65, Th10, FUNCT_2:65;

va in A1 by A71, STRUCT_0:def 5;

then va in A1 + B1 by VECTSP_5:2;

then ua + va in A1 + B1 by A70, VECTSP_4:20;

then ua + va in the carrier of (A1 + B1) by STRUCT_0:def 5;

then f . (ua + va) in f .: the carrier of (A1 + B1) by FUNCT_2:35;

hence x in f .: the carrier of (A1 + B1) by A1, A67, A72, A69, VECTSP_1:def 20; :: thesis: verum

assume x in the carrier of P ; :: thesis: x in the carrier of AB

then A73: 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 A64, 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 A74: 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

A75: c in the carrier of (A1 + B1) and

A76: x = f . c by A74, FUNCT_2:65;

c in A1 + B1 by A75, STRUCT_0:def 5;

then consider u, v being Element of A such that

A77: u in A1 and

A78: v in B1 and

A79: c = u + v by VECTSP_5:1;

v in the carrier of B1 by A78, STRUCT_0:def 5;

then A80: f . v in Lin (f .: the carrier of B1) by FUNCT_2:35, VECTSP_7:8;

u in the carrier of A1 by A77, STRUCT_0:def 5;

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

x = (f . u) + (f . v) by A1, A76, A79, VECTSP_1:def 20;

then x in (Lin (f .: the carrier of A1)) + (Lin (f .: the carrier of B1)) by A81, A80, VECTSP_5:1;

hence x in the carrier of (A3 + B3) by A52, A34, STRUCT_0:def 5; :: thesis: verum

end;assume A74: 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

A75: c in the carrier of (A1 + B1) and

A76: x = f . c by A74, FUNCT_2:65;

c in A1 + B1 by A75, STRUCT_0:def 5;

then consider u, v being Element of A such that

A77: u in A1 and

A78: v in B1 and

A79: c = u + v by VECTSP_5:1;

v in the carrier of B1 by A78, STRUCT_0:def 5;

then A80: f . v in Lin (f .: the carrier of B1) by FUNCT_2:35, VECTSP_7:8;

u in the carrier of A1 by A77, STRUCT_0:def 5;

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

x = (f . u) + (f . v) by A1, A76, A79, VECTSP_1:def 20;

then x in (Lin (f .: the carrier of A1)) + (Lin (f .: the carrier of B1)) by A81, A80, VECTSP_5:1;

hence x in the carrier of (A3 + B3) by A52, A34, STRUCT_0:def 5; :: thesis: verum

hence x in the carrier of AB by A53, A73, Th10; :: thesis: verum

then A82: P = AB by VECTSP_4:29;

(FuncLatt f) . (a "\/" b) = (FuncLatt f) . (A1 + B1) by A5, A2, Th7;

hence (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) by A30, A3, A28, A52, A34, A82, Th7; :: thesis: verum