let K be Field; :: thesis: for T being K -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is distributive
let T be K -monomorphic comRing; :: thesis: for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is distributive
let f be Monomorphism of K,T; :: thesis: ( K,T are_disjoint implies embField f is distributive )
assume AS: K,T are_disjoint ; :: thesis: embField f is distributive

now :: thesis: for a, b, c being Element of (embField f) holds
( a * (b + c) = (a * b) + (a * c) & (b + c) * a = (b * a) + (c * a) )

let a, b, c be Element of (embField f); :: thesis: ( b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) )
reconsider x = a, y = b, z = c as Element of carr f by defemb;

per cases ( a = 0. K or a <> 0. K ) ;

suppose A: a = 0. K ; :: thesis: ( b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) )

A1: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= 0. K by A, defmultf ;
A2: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= 0. K by A, defmultf ;
reconsider bc = b + c as Element of carr f by defemb;
thus I: a * (b + c) = (multemb f) . (x,(b + c)) by defemb
.= multemb (f,x,bc) by defmult
.= 0. K by A, defmultf
.= 0. (embField f) by defemb
.= (0. (embField f)) + (0. (embField f)) by RLVECT_1:def 4
.= (a * b) + (0. (embField f)) by A1, defemb
.= (a * b) + (a * c) by A2, defemb ; :: thesis: (b + c) * a = (b * a) + (c * a)
thus (b + c) * a = a * (b + c) by GROUP_1:def 12
.= (b * a) + (a * c) by I, GROUP_1:def 12
.= (b * a) + (c * a) by GROUP_1:def 12 ; :: thesis: verum

end;

suppose A: a <> 0. K ; :: thesis: ( b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) )

thus I: a * (b + c) = (a * b) + (a * c) :: thesis: (b + c) * a = (b * a) + (c * a)

proof

per cases ( b = 0. K or c = 0. K or ( b <> 0. K & c <> 0. K ) ) ;

suppose B: b = 0. K ; :: thesis: a * (b + c) = (a * b) + (a * c)

A1: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= 0. K by B, defmultf ;
b + c = (0. (embField f)) + c by B, defemb
.= c by RLVECT_1:def 4 ;
hence a * (b + c) = (0. (embField f)) + (a * c) by RLVECT_1:def 4
.= (a * b) + (a * c) by A1, defemb ;
:: thesis: verum

end;

suppose C: c = 0. K ; :: thesis: a * (b + c) = (a * b) + (a * c)

A1: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= 0. K by C, defmultf ;
b + c = b + (0. (embField f)) by C, defemb
.= b by RLVECT_1:def 4 ;
hence a * (b + c) = (a * b) + (0. (embField f)) by RLVECT_1:def 4
.= (a * b) + (a * c) by A1, defemb ;
:: thesis: verum

end;

suppose BC: ( b <> 0. K & c <> 0. K ) ; :: thesis: a * (b + c) = (a * b) + (a * c)

per cases ( x in [#] K or not x in [#] K ) ;

suppose X: x in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider a1 = a as Element of K ;

per cases ( y in [#] K or not y in [#] K ) ;

suppose Y: y in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider b1 = b as Element of K ;
A1: a * b = a1 * b1 by Lm11;
reconsider ab = a * b as Element of carr f by defemb;

per cases ( c in [#] K or not z in [#] K ) ;

suppose c in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of K ;
A2: a * c = a1 * c1 by Lm11;
A3: b + c = b1 + c1 by Lm7;
reconsider bc = b + c, ac = a * c as Element of carr f by defemb;
thus a * (b + c) = a1 * (b1 + c1) by A3, Lm11
.= (a1 * b1) + (a1 * c1) by VECTSP_1:def 7
.= (a * b) + (a * c) by A2, A1, Lm7 ; :: thesis: verum

end;

suppose Z: not z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of T by Lm1;
A2: a * c = (f . a1) * c1 by AS, X, Z, A, Lm10;
A3: b + c = (f . b1) + c1 by AS, Y, Z, Lm6;
then reconsider bc = (f . b1) + c1 as Element of carr f by defemb;
reconsider ac = (f . a1) * c1 as Element of carr f by A2, defemb;
A4: not bc in [#] K by AS, A3, Y, Z, Lm6;
A5: not ac in [#] K by A2, AS, A, X, Z, Lm10;
thus a * (b + c) = (multemb f) . (x,bc) by A3, defemb
.= multemb (f,x,bc) by defmult
.= (f . a1) * ((f . b1) + c1) by A, A4, defmultf
.= ((f . a1) * (f . b1)) + ((f . a1) * c1) by VECTSP_1:def 7
.= (f . (a1 * b1)) + ((f . a1) * c1) by GROUP_6:def 6
.= addemb (f,ab,ac) by A5, A1, defaddf
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by A2, defemb ; :: thesis: verum

end;

end;

end;

suppose Y: not y in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider b1 = b as Element of T by Lm1;
A1: a * b = (f . a1) * b1 by AS, X, Y, A, Lm10;
then reconsider ab = (f . a1) * b1 as Element of carr f by defemb;
A5: not ab in [#] K by A1, AS, X, Y, A, Lm10;

per cases ( z in [#] K or not z in [#] K ) ;

suppose Z: z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of K ;
A2: a * c = a1 * c1 by Lm11;
A3: b + c = b1 + (f . c1) by AS, Y, Z, Lm6;
reconsider bc = b + c, ac = a * c as Element of carr f by defemb;
A4: not bc in [#] K by AS, Y, Z, Lm6;
reconsider fc1 = f . c1 as Element of T ;
thus a * (b + c) = (multemb f) . (x,bc) by defemb
.= multemb (f,x,bc) by defmult
.= (f . a1) * (b1 + (f . c1)) by A, A3, A4, defmultf
.= ((f . a1) * b1) + ((f . a1) * (f . c1)) by VECTSP_1:def 7
.= ((f . a1) * b1) + (f . (a1 * c1)) by GROUP_6:def 6
.= addemb (f,ab,ac) by A5, A2, defaddf
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by A1, defemb ; :: thesis: verum

end;

suppose Z: not z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of T by Lm1;
A2: a * c = (f . a1) * c1 by AS, X, Z, A, Lm10;
reconsider ac = a * c as Element of carr f by defemb;
A6: not ac in [#] K by AS, X, Z, A, Lm10;

per cases ( not the addF of T . (y,z) in rng f or the addF of T . (y,z) in rng f ) ;

suppose Z1: not the addF of T . (y,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

then A3: b + c = b1 + c1 by AS, Y, Z, Lm8;
reconsider bc = b + c as Element of carr f by defemb;
A4: not bc in [#] K by AS, A3, XBOOLE_0:def 4;
then A8: the multF of T . ((f . x),bc) in ([#] T) \ (rng f) by A, X, Lm5;
the multF of T . ((f . x),bc) = (f . a1) * (b1 + c1) by Z1, AS, Y, Z, Lm8
.= ((f . a1) * b1) + ((f . a1) * c1) by VECTSP_1:def 7
.= the addF of T . (ab,ac) by AS, X, Z, A, Lm10 ;
then A7: not the addF of T . (ab,ac) in rng f by A8, XBOOLE_0:def 5;
thus a * (b + c) = (multemb f) . (x,bc) by defemb
.= multemb (f,x,bc) by defmult
.= (f . a1) * (b1 + c1) by A, A3, A4, defmultf
.= ((f . a1) * b1) + ((f . a1) * c1) by VECTSP_1:def 7
.= addemb (f,ab,ac) by A2, A5, A6, A7, defaddf
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by A1, defemb ; :: thesis: verum

end;

suppose Z1: the addF of T . (y,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

then A3: b + c = (f ") . (b1 + c1) by Y, Z, Lm9;
reconsider bc = b + c, ac = a * c as Element of carr f by defemb;
A0: dom f = [#] K by FUNCT_2:def 1;
b1 + c1 in dom (f ") by Z1, FUNCT_1:33;
then b + c in rng (f ") by A3, FUNCT_1:3;
then reconsider bc1 = b + c as Element of K ;
A9: f . (a1 * bc1) = (f . a1) * (f . bc1) by GROUP_6:def 6
.= (f . a1) * (b1 + c1) by Z1, A3, FUNCT_1:35
.= ((f . a1) * b1) + ((f . a1) * c1) by VECTSP_1:def 7 ;
then A4: the addF of T . (ab,ac) in rng f by A0, A2, FUNCT_1:def 3;
reconsider fa1 = f . a1 as Element of rng f by A0, FUNCT_1:3;
reconsider fbc1 = f . bc1 as Element of rng f by A0, FUNCT_1:3;
thus a * (b + c) = (multemb f) . (x,bc) by defemb
.= multemb (f,x,bc) by defmult
.= a1 * bc1 by defmultf
.= (f ") . (((f . a1) * b1) + ((f . a1) * c1)) by A9, A0, FUNCT_1:34
.= addemb (f,ab,ac) by A2, A4, A5, A6, defaddf
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by A1, defemb ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose X: not x in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider a1 = a as Element of T by Lm1;
B0: dom f = [#] K by FUNCT_2:def 1;

per cases ( y in [#] K or not y in [#] K ) ;

suppose Y: y in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider b1 = b as Element of K ;
A1: a * b = a1 * (f . b1) by AS, X, Y, BC, Lm10;
then reconsider ab = a1 * (f . b1) as Element of carr f by defemb;
A2: not ab in [#] K by A1, AS, X, Y, BC, Lm10;

per cases ( z in [#] K or not z in [#] K ) ;

suppose Z: z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of K ;
A3: a * c = a1 * (f . c1) by AS, X, Z, BC, Lm10;
then reconsider ac = a1 * (f . c1) as Element of carr f by defemb;
A4: not ac in [#] K by A3, AS, X, Z, BC, Lm10;
A5: b + c = (addemb f) . (y,z) by defemb
.= addemb (f,y,z) by defadd
.= b1 + c1 by defaddf ;
then reconsider bc1 = b + c as Element of K ;
reconsider bc = b + c as Element of carr f by defemb;

per cases ( bc = 0. K or bc <> 0. K ) ;

suppose O: bc = 0. K ; :: thesis: a * (b + c) = (a * b) + (a * c)

A6: a * (b + c) = (multemb f) . (x,bc) by defemb
.= multemb (f,x,bc) by defmult
.= 0. K by O, defmultf ;
(a1 * (f . b1)) + (a1 * (f . c1)) = a1 * ((f . b1) + (f . c1)) by VECTSP_1:def 7
.= a1 * (f . (b1 + c1)) by VECTSP_1:def 20
.= a1 * (0. T) by O, RING_2:6, A5
.= f . (0. K) by RING_2:6 ;
then A7: (a1 * (f . b1)) + (a1 * (f . c1)) in rng f by B0, FUNCT_1:3;
(a * b) + (a * c) = (addemb f) . (ab,ac) by A1, A3, defemb
.= addemb (f,ab,ac) by defadd
.= (f ") . ((a1 * (f . b1)) + (a1 * (f . c1))) by A4, A2, A7, defaddf
.= (f ") . (a1 * ((f . b1) + (f . c1))) by VECTSP_1:def 7
.= (f ") . (a1 * (f . (b1 + c1))) by VECTSP_1:def 20
.= (f ") . (a1 * (0. T)) by A5, O, RING_2:6
.= 0. K by Th3 ;
hence a * (b + c) = (a * b) + (a * c) by A6; :: thesis: verum

end;

suppose O: bc <> 0. K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then A6: the multF of T . (x,(f . bc)) in ([#] T) \ (rng f) by A5, X, Lm4;
the multF of T . (x,(f . bc)) = a1 * ((f . b1) + (f . c1)) by A5, VECTSP_1:def 20
.= (a1 * (f . b1)) + (a1 * (f . c1)) by VECTSP_1:def 7 ;
then A7: not (a1 * (f . b1)) + (a1 * (f . c1)) in rng f by A6, XBOOLE_0:def 5;
thus a * (b + c) = (multemb f) . (x,bc) by defemb
.= multemb (f,x,bc) by defmult
.= a1 * (f . bc1) by O, X, defmultf
.= a1 * ((f . b1) + (f . c1)) by A5, VECTSP_1:def 20
.= (a1 * (f . b1)) + (a1 * (f . c1)) by VECTSP_1:def 7
.= addemb (f,ab,ac) by A2, A4, A7, defaddf
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by A1, A3, defemb ; :: thesis: verum

end;

end;

end;

suppose Z: not z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of T by Lm1;
A3: b + c = (f . b1) + c1 by AS, Y, Z, Lm6;
then reconsider bc = (f . b1) + c1 as Element of carr f by defemb;
A4: not bc in [#] K by A3, AS, Lm6, Z, Y;
A7: the multF of T . (x,bc) = a1 * ((f . b1) + c1)
.= (a1 * (f . b1)) + (a1 * c1) by VECTSP_1:def 7 ;

per cases ( the multF of T . (x,bc) in rng f or not the multF of T . (x,bc) in rng f ) ;

suppose Z1: the multF of T . (x,bc) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

A5: now :: thesis: not the multF of T . (x,z) in rng f

assume the multF of T . (x,z) in rng f ; :: thesis: contradiction
then consider yy being object such that
C1: ( yy in dom f & f . yy = a1 * c1 ) by FUNCT_1:def 3;
reconsider yy = yy as Element of carr f by C1, XBOOLE_0:def 3;
the addF of T . (ab,(f . yy)) in ([#] T) \ (rng f) by C1, A2, Lm2;
hence contradiction by Z1, A7, C1, XBOOLE_0:def 5; :: thesis: verum

end;

then A6: a * c = a1 * c1 by AS, X, Z, Lm12;
then reconsider ac = a1 * c1 as Element of carr f by defemb;
A9: not ac in [#] K by A6, AS, X, Z, A5, Lm12;
thus a * (b + c) = (multemb f) . (x,bc) by A3, defemb
.= multemb (f,x,bc) by defmult
.= (f ") . (a1 * ((f . b1) + c1)) by Z1, A4, X, defmultf
.= addemb (f,ab,ac) by defaddf, Z1, A7, A2, A9
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by A1, A6, defemb ; :: thesis: verum

end;

suppose Z1: not the multF of T . (x,bc) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

A9: ( not x = 0. K & not bc = 0. K ) by X, A3, AS, Lm6, Z, Y;
A10: a * (b + c) = (multemb f) . (x,bc) by A3, defemb
.= multemb (f,x,bc) by defmult
.= a1 * ((f . b1) + c1) by X, A4, Z1, A9, defmultf
.= (a1 * (f . b1)) + (a1 * c1) by VECTSP_1:def 7 ;

per cases ( the multF of T . (x,z) in rng f or not the multF of T . (x,z) in rng f ) ;

suppose Z2: the multF of T . (x,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

A7: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by X, Z2, Z, defmultf ;
then reconsider ac = (f ") . (a1 * c1) as Element of carr f by defemb;
a1 * c1 in dom (f ") by Z2, FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = ac as Element of K ;
(a * b) + (a * c) = (addemb f) . (ab,ac) by A1, A7, defemb
.= addemb (f,ab,ac) by defadd
.= (a1 * (f . b1)) + (f . ac1) by defaddf, A2 ;
hence a * (b + c) = (a * b) + (a * c) by A10, Z2, FUNCT_1:35; :: thesis: verum

end;

suppose Z2: not the multF of T . (x,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

A9: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by X, Z2, A, BC, Z, defmultf ;
then reconsider ac = a1 * c1 as Element of carr f by defemb;
A8: not ac in [#] K by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by A1, A9, defemb
.= addemb (f,ab,ac) by defadd
.= a * (b + c) by defaddf, A2, A7, A8, Z1, A10 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose Y: not y in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider b1 = b as Element of T by Lm1;

per cases ( z in [#] K or not z in [#] K ) ;

suppose Z: z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of K ;
B1: b + c = b1 + (f . c1) by AS, Y, Z, Lm6;
then reconsider bc = b1 + (f . c1) as Element of carr f by defemb;
B2: not bc in [#] K by Y, Z, AS, Lm6, B1;
B3: a * c = a1 * (f . c1) by AS, X, Z, BC, Lm10;
then reconsider ac = a1 * (f . c1) as Element of carr f by defemb;
B4: not ac in [#] K by B3, X, Z, BC, AS, Lm10;

per cases ( not the multF of T . (x,y) in rng f or the multF of T . (x,y) in rng f ) ;

suppose Z1: not the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B5: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= a1 * b1 by Z1, X, Y, A, BC, defmultf ;
then reconsider ab = a1 * b1 as Element of carr f by defemb;
B6: not ab in [#] K by AS, XBOOLE_0:def 4;
Z3: the addF of T . (ab,ac) = (a1 * b1) + (a1 * (f . c1))
.= a1 * (b1 + (f . c1)) by VECTSP_1:def 7
.= the multF of T . (x,bc) ;

per cases ( the multF of T . (x,bc) in rng f or not the multF of T . (x,bc) in rng f ) ;

suppose Z2: the multF of T . (x,bc) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

thus a * (b + c) = (multemb f) . (x,bc) by B1, defemb
.= multemb (f,x,bc) by defmult
.= (f ") . (a1 * (b1 + (f . c1))) by Z2, B2, X, defmultf
.= addemb (f,ab,ac) by defaddf, Z2, Z3, B4, B6
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by B3, B5, defemb ; :: thesis: verum

end;

suppose Z2: not the multF of T . (x,bc) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B7: ( x <> 0. K & bc <> 0. K ) by X, Y, Z, AS, Lm6, B1;
thus a * (b + c) = (multemb f) . (x,bc) by B1, defemb
.= multemb (f,x,bc) by defmult
.= a1 * (b1 + (f . c1)) by B7, X, B2, Z2, defmultf
.= addemb (f,ab,ac) by defaddf, Z2, Z3, B4, B6
.= (addemb f) . (ab,ac) by defadd
.= (a * b) + (a * c) by B3, B5, defemb ; :: thesis: verum

end;

end;

end;

suppose Z1: the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B5: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= (f ") . (a1 * b1) by Z1, X, Y, defmultf ;
a1 * b1 in dom (f ") by Z1, FUNCT_1:33;
then (f ") . (a1 * b1) in rng (f ") by FUNCT_1:def 3;
then reconsider ab1 = (f ") . (a1 * b1) as Element of K ;
reconsider ab = ab1 as Element of carr f by B5, defemb;
the addF of T . ((f . ab),ac) in ([#] T) \ (rng f) by Lm3, B4;
then B7: not the addF of T . ((f . ab),ac) in rng f by XBOOLE_0:def 5;

B9: now :: thesis: not the multF of T . (x,bc) in rng f

assume the multF of T . (x,bc) in rng f ; :: thesis: contradiction
then consider yy being object such that
C1: ( yy in dom f & f . yy = a1 * (b1 + (f . c1)) ) by FUNCT_1:def 3;
f . yy = (a1 * b1) + (a1 * (f . c1)) by C1, VECTSP_1:def 7
.= (f . ab1) + (a1 * (f . c1)) by Z1, FUNCT_1:35 ;
hence contradiction by B7, C1, FUNCT_1:def 3; :: thesis: verum

end;

B10: ( a <> 0. K & bc <> 0. K ) by X, Y, Z, AS, Lm6, B1;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B5, B3, defemb
.= addemb (f,ab,ac) by defadd
.= (f . ab1) + (a1 * (f . c1)) by defaddf, B4
.= (a1 * b1) + (a1 * (f . c1)) by Z1, FUNCT_1:35
.= a1 * (b1 + (f . c1)) by VECTSP_1:def 7
.= multemb (f,x,bc) by B10, X, B2, B9, defmultf
.= (multemb f) . (x,bc) by defmult
.= a * (b + c) by B1, defemb ; :: thesis: verum

end;

end;

end;

suppose Z: not z in [#] K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then reconsider c1 = c as Element of T by Lm1;

per cases ( the addF of T . (y,z) in rng f or not the addF of T . (y,z) in rng f ) ;

suppose Z1: the addF of T . (y,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B1: b + c = (addemb f) . (y,z) by defemb
.= addemb (f,y,z) by defadd
.= (f ") . (b1 + c1) by Y, Z, Z1, defaddf ;
b1 + c1 in dom (f ") by Z1, FUNCT_1:33;
then (f ") . (b1 + c1) in rng (f ") by FUNCT_1:def 3;
then reconsider bc1 = (f ") . (b1 + c1) as Element of K ;
reconsider bc = bc1 as Element of carr f by B1, defemb;
B0: dom f = [#] K by FUNCT_2:def 1;

per cases ( bc = 0. K or bc <> 0. K ) ;

suppose B5: bc = 0. K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then B2: b1 + c1 = 0. T by Z1, Th2;
B3: a * (b + c) = (multemb f) . (x,bc) by B1, defemb
.= multemb (f,x,bc) by defmult
.= 0. K by B5, defmultf ;
A6: (a1 * b1) + (a1 * c1) = a1 * (0. T) by B2, VECTSP_1:def 7
.= f . (0. K) by RING_2:6 ;
then A7: (a1 * b1) + (a1 * c1) in rng f by B0, FUNCT_1:3;

per cases ( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f ) ;

suppose Z2: the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= (f ") . (a1 * b1) by Y, X, Z2, defmultf ;
a1 * b1 in dom (f ") by Z2, FUNCT_1:33;
then (f ") . (a1 * b1) in rng (f ") by FUNCT_1:def 3;
then reconsider ab1 = (f ") . (a1 * b1) as Element of K ;
reconsider ab = ab1 as Element of carr f by B4, defemb;
U: f . ((0. K) - ab1) = (f . (0. K)) - (f . ab1) by RING_2:8
.= ((a1 * b1) + (a1 * c1)) - (a1 * b1) by A6, Z2, FUNCT_1:35
.= (a1 * c1) + ((a1 * b1) - (a1 * b1)) by RLVECT_1:def 3
.= (a1 * c1) + (0. T) by RLVECT_1:15
.= the multF of T . (x,z) ;
then Z3: the multF of T . (x,z) in rng f by B0, FUNCT_1:def 3;
B5: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by Z, X, Z3, defmultf ;
B11: a1 * c1 in rng f by U, B0, FUNCT_1:def 3;
then a1 * c1 in dom (f ") by FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = (f ") . (a1 * c1) as Element of K ;
reconsider ac = ac1 as Element of carr f by B5, defemb;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B5, defemb
.= addemb (f,ab,ac) by defadd
.= ab1 + ac1 by defaddf
.= (f ") . ((a1 * b1) + (a1 * c1)) by B11, Z2, Th1
.= a * (b + c) by A6, B3, B0, FUNCT_1:34 ; :: thesis: verum

end;

suppose Z2: not the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= a1 * b1 by A, BC, Y, X, Z2, defmultf ;
a1 * b1 in ([#] T) \ (rng f) by Z2, XBOOLE_0:def 5;
then reconsider ab = a1 * b1 as Element of carr f by XBOOLE_0:def 3;
B9: not ab in [#] K by AS, XBOOLE_0:def 4;

Z3: now :: thesis: not the multF of T . (x,z) in rng f

assume Z3: the multF of T . (x,z) in rng f ; :: thesis: contradiction
B5: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by Z, X, Z3, defmultf ;
a1 * c1 in dom (f ") by Z3, FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = (f ") . (a1 * c1) as Element of K ;
reconsider ac = ac1 as Element of carr f by B5, defemb;
B12: the addF of T . (ab,(f . ac)) in ([#] T) \ (rng f) by B9, Lm2;
the addF of T . (ab,(f . ac)) = (a1 * b1) + (a1 * c1) by Z3, FUNCT_1:35;
hence contradiction by B12, A7, XBOOLE_0:def 5; :: thesis: verum

end;

B5: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by A, BC, Z, X, Z3, defmultf ;
a1 * c1 in ([#] T) \ (rng f) by Z3, XBOOLE_0:def 5;
then reconsider ac = a1 * c1 as Element of carr f by XBOOLE_0:def 3;
B13: not ac in [#] K by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B5, defemb
.= addemb (f,ab,ac) by defadd
.= (f ") . ((a1 * b1) + (a1 * c1)) by A7, B9, B13, defaddf
.= a * (b + c) by A6, B3, B0, FUNCT_1:34 ; :: thesis: verum

end;

end;

end;

suppose B5: bc <> 0. K ; :: thesis: a * (b + c) = (a * b) + (a * c)

then B12: the multF of T . (x,(f . bc)) in ([#] T) \ (rng f) by X, Lm4;
B3: a * (b + c) = (multemb f) . (x,bc) by B1, defemb
.= multemb (f,x,bc) by defmult
.= a1 * (f . bc1) by B5, X, defmultf
.= a1 * (b1 + c1) by Z1, FUNCT_1:35
.= (a1 * b1) + (a1 * c1) by VECTSP_1:def 7 ;

per cases ( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f ) ;

suppose Z2: the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= (f ") . (a1 * b1) by Y, X, Z2, defmultf ;
a1 * b1 in dom (f ") by Z2, FUNCT_1:33;
then (f ") . (a1 * b1) in rng (f ") by FUNCT_1:def 3;
then reconsider ab1 = (f ") . (a1 * b1) as Element of K ;
reconsider ab = ab1 as Element of carr f by B4, defemb;

B7: now :: thesis: not the multF of T . (x,z) in rng f

assume the multF of T . (x,z) in rng f ; :: thesis: contradiction
then consider xx being object such that
C1: ( xx in dom f & f . xx = a1 * c1 ) by FUNCT_1:def 3;
reconsider xx = xx as Element of K by C1;
consider yy being object such that
C2: ( yy in dom f & f . yy = a1 * b1 ) by Z2, FUNCT_1:def 3;
reconsider yy = yy as Element of K by C2;
C3: dom f = [#] K by FUNCT_2:def 1;
the multF of T . (x,(f . bc)) = a1 * (b1 + c1) by Z1, FUNCT_1:35
.= (f . yy) + (f . xx) by C1, C2, VECTSP_1:def 7
.= f . (xx + yy) by VECTSP_1:def 20 ;
then the multF of T . (x,(f . bc)) in rng f by C3, FUNCT_1:def 3;
hence contradiction by B12, XBOOLE_0:def 5; :: thesis: verum

end;

B8: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by Z, B7, A, BC, X, defmultf ;
a1 * c1 in ([#] T) \ (rng f) by B7, XBOOLE_0:def 5;
then reconsider ac = a1 * c1 as Element of carr f by XBOOLE_0:def 3;
B9: not ac in [#] K by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B8, defemb
.= addemb (f,ab,ac) by defadd
.= (f . ab1) + (a1 * c1) by defaddf, B9
.= a * (b + c) by B3, Z2, FUNCT_1:35 ; :: thesis: verum

end;

suppose Z2: not the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= a1 * b1 by A, BC, Y, X, Z2, defmultf ;
then reconsider ab = a1 * b1 as Element of carr f by defemb;
B5: not ab in [#] K by AS, XBOOLE_0:def 4;

per cases ( the multF of T . (x,z) in rng f or not the multF of T . (x,z) in rng f ) ;

suppose Z3: the multF of T . (x,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B8: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by Z, X, Z3, defmultf ;
a1 * c1 in dom (f ") by Z3, FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = (f ") . (a1 * c1) as Element of K ;
reconsider ac = ac1 as Element of carr f by B8, defemb;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B8, defemb
.= addemb (f,ab,ac) by defadd
.= (a1 * b1) + (f . ac1) by defaddf, B5
.= a * (b + c) by B3, Z3, FUNCT_1:35 ; :: thesis: verum

end;

suppose Z3: not the multF of T . (x,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B8: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by Z, Z3, A, BC, X, defmultf ;
a1 * c1 in ([#] T) \ (rng f) by Z3, XBOOLE_0:def 5;
then reconsider ac = a1 * c1 as Element of carr f by XBOOLE_0:def 3;
B9: not ac in [#] K by AS, XBOOLE_0:def 4;
the multF of T . (x,(f . bc)) = a1 * (b1 + c1) by Z1, FUNCT_1:35
.= (a1 * b1) + (a1 * c1) by VECTSP_1:def 7
.= the addF of T . (ab,ac) ;
then B10: not the addF of T . (ab,ac) in rng f by B12, XBOOLE_0:def 5;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B8, defemb
.= addemb (f,ab,ac) by defadd
.= a * (b + c) by defaddf, B9, B5, B10, B3 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose Z1: not the addF of T . (y,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B1: b + c = (addemb f) . (y,z) by defemb
.= addemb (f,y,z) by defadd
.= b1 + c1 by Y, Z, Z1, defaddf ;
b1 + c1 in ([#] T) \ (rng f) by Z1, XBOOLE_0:def 5;
then reconsider bc = b1 + c1 as Element of carr f by XBOOLE_0:def 3;
B2: not bc in [#] K by AS, XBOOLE_0:def 4;
B5: not bc = 0. K by AS, XBOOLE_0:def 4;

per cases ( the multF of T . (x,bc) in rng f or not the multF of T . (x,bc) in rng f ) ;

suppose Z2: the multF of T . (x,bc) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B3: a * (b + c) = (multemb f) . (x,bc) by B1, defemb
.= multemb (f,x,bc) by defmult
.= (f ") . (a1 * (b1 + c1)) by Z2, B2, X, defmultf
.= (f ") . ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7 ;

per cases ( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f ) ;

suppose Z3: the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= (f ") . (a1 * b1) by Y, X, Z3, defmultf ;
a1 * b1 in dom (f ") by Z3, FUNCT_1:33;
then (f ") . (a1 * b1) in rng (f ") by FUNCT_1:def 3;
then reconsider ab1 = (f ") . (a1 * b1) as Element of K ;
reconsider ab = ab1 as Element of carr f by B4, defemb;
B6: the multF of T . (x,z) in rng f

proof

the multF of T . (x,bc) = a1 * (b1 + c1)
.= (a1 * b1) + (a1 * c1) by VECTSP_1:def 7 ;
then consider xx being object such that
C1: ( xx in dom f & f . xx = (a1 * b1) + (a1 * c1) ) by Z2, FUNCT_1:def 3;
reconsider xx = xx as Element of K by C1;
consider yy being object such that
C2: ( yy in dom f & f . yy = a1 * b1 ) by Z3, FUNCT_1:def 3;
reconsider yy = yy as Element of K by C2;
C3: f . (xx - yy) = (f . xx) - (f . yy) by RING_2:8
.= (a1 * c1) + ((a1 * b1) + (- (a1 * b1))) by C1, C2, RLVECT_1:def 3
.= (a1 * c1) + (0. T) by RLVECT_1:5 ;
[#] K = dom f by FUNCT_2:def 1;
hence the multF of T . (x,z) in rng f by C3, FUNCT_1:def 3; :: thesis: verum

end;

B7: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by X, Z, B6, defmultf ;
a1 * c1 in dom (f ") by B6, FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = (f ") . (a1 * c1) as Element of K ;
reconsider ac = ac1 as Element of carr f by B7, defemb;
reconsider abr = a1 * b1 as Element of rng f by Z3;
reconsider acr = a1 * c1 as Element of rng f by B6;
B8: ((f ") . abr) + ((f ") . acr) = (f ") . ((a1 * b1) + (a1 * c1)) by Th1;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B7, defemb
.= addemb (f,ab,ac) by defadd
.= a * (b + c) by defaddf, B8, B3 ; :: thesis: verum

end;

suppose Z3: not the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= a1 * b1 by A, BC, Y, X, Z3, defmultf ;
a1 * b1 in ([#] T) \ (rng f) by Z3, XBOOLE_0:def 5;
then reconsider ab = a1 * b1 as Element of carr f by XBOOLE_0:def 3;
reconsider ab1 = ab as Element of T ;
B6: not ab in [#] K by AS, XBOOLE_0:def 4;

Z4: now :: thesis: not the multF of T . (x,z) in rng f

assume Z4a: the multF of T . (x,z) in rng f ; :: thesis: contradiction
B7: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by Z4a, X, Z, defmultf ;
a1 * c1 in dom (f ") by Z4a, FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = (f ") . (a1 * c1) as Element of K ;
reconsider ac = ac1 as Element of carr f by B7, defemb;
U: the addF of T . (ab,(f . ac)) in ([#] T) \ (rng f) by B6, Lm2;
f . ac1 = a1 * c1 by Z4a, FUNCT_1:35;
then ab1 + (f . ac1) = a1 * (b1 + c1) by VECTSP_1:def 7
.= the multF of T . (x,bc) ;
hence contradiction by U, Z2, XBOOLE_0:def 5; :: thesis: verum

end;

B7: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by Z4, A, BC, X, Z, defmultf ;
a1 * c1 in ([#] T) \ (rng f) by Z4, XBOOLE_0:def 5;
then reconsider ac = a1 * c1 as Element of carr f by XBOOLE_0:def 3;
reconsider ac1 = ac as Element of T ;
B9: not ac in [#] K by AS, XBOOLE_0:def 4;
B10: (a1 * b1) + (a1 * c1) = a1 * (b1 + c1) by VECTSP_1:def 7
.= the multF of T . (x,bc) ;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B7, defemb
.= addemb (f,ab,ac) by defadd
.= a * (b + c) by defaddf, B6, B9, B10, Z2, B3 ; :: thesis: verum

end;

end;

end;

suppose Z2: not the multF of T . (x,bc) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B3: a * (b + c) = (multemb f) . (x,bc) by B1, defemb
.= multemb (f,x,bc) by defmult
.= a1 * (b1 + c1) by A, Z2, B2, B5, X, defmultf
.= (a1 * b1) + (a1 * c1) by VECTSP_1:def 7 ;

per cases ( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f ) ;

suppose Z3: the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= (f ") . (a1 * b1) by Y, X, Z3, defmultf ;
a1 * b1 in dom (f ") by Z3, FUNCT_1:33;
then (f ") . (a1 * b1) in rng (f ") by FUNCT_1:def 3;
then reconsider ab1 = (f ") . (a1 * b1) as Element of K ;
reconsider ab = ab1 as Element of carr f by B4, defemb;

Z4: now :: thesis: not the multF of T . (x,z) in rng f

assume the multF of T . (x,z) in rng f ; :: thesis: contradiction
then consider yy being object such that
C1: ( yy in dom f & f . yy = a1 * c1 ) by FUNCT_1:def 3;
reconsider yy = yy as Element of K by C1;
C2: the multF of T . (x,bc) = a1 * (b1 + c1)
.= (a1 * b1) + (a1 * c1) by VECTSP_1:def 7 ;
C3: f . (ab1 + yy) = (f . ab1) + (f . yy) by VECTSP_1:def 20
.= (a1 * b1) + (a1 * c1) by C1, Z3, FUNCT_1:35 ;
[#] K = dom f by FUNCT_2:def 1;
hence contradiction by C3, C2, Z2, FUNCT_1:def 3; :: thesis: verum

end;

B5: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by A, BC, Z, X, Z4, defmultf ;
a1 * c1 in ([#] T) \ (rng f) by Z4, XBOOLE_0:def 5;
then reconsider ac = a1 * c1 as Element of carr f by XBOOLE_0:def 3;
B9: not ac in [#] K by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B5, defemb
.= addemb (f,ab,ac) by defadd
.= (f . ab1) + (a1 * c1) by defaddf, B9
.= a * (b + c) by B3, Z3, FUNCT_1:35 ; :: thesis: verum

end;

suppose Z3: not the multF of T . (x,y) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B4: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= a1 * b1 by A, BC, Y, X, Z3, defmultf ;
a1 * b1 in ([#] T) \ (rng f) by Z3, XBOOLE_0:def 5;
then reconsider ab = a1 * b1 as Element of carr f by XBOOLE_0:def 3;
B9: not ab in [#] K by AS, XBOOLE_0:def 4;

per cases ( the multF of T . (x,z) in rng f or not the multF of T . (x,z) in rng f ) ;

suppose Z4: the multF of T . (x,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B5: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= (f ") . (a1 * c1) by Z, X, Z4, defmultf ;
a1 * c1 in dom (f ") by Z4, FUNCT_1:33;
then (f ") . (a1 * c1) in rng (f ") by FUNCT_1:def 3;
then reconsider ac1 = (f ") . (a1 * c1) as Element of K ;
reconsider ac = ac1 as Element of carr f by B5, defemb;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B5, defemb
.= addemb (f,ab,ac) by defadd
.= (a1 * b1) + (f . ac1) by defaddf, B9
.= a * (b + c) by B3, Z4, FUNCT_1:35 ; :: thesis: verum

end;

suppose Z4: not the multF of T . (x,z) in rng f ; :: thesis: a * (b + c) = (a * b) + (a * c)

B5: a * c = (multemb f) . (x,z) by defemb
.= multemb (f,x,z) by defmult
.= a1 * c1 by A, BC, Z, X, Z4, defmultf ;
a1 * c1 in ([#] T) \ (rng f) by Z4, XBOOLE_0:def 5;
then reconsider ac = a1 * c1 as Element of carr f by XBOOLE_0:def 3;
B19: not ac in [#] K by AS, XBOOLE_0:def 4;
B20: the addF of T . (ab,ac) = (a1 * b1) + (a1 * c1)
.= a1 * (b1 + c1) by VECTSP_1:def 7
.= the multF of T . (x,bc) ;
thus (a * b) + (a * c) = (addemb f) . (ab,ac) by B4, B5, defemb
.= addemb (f,ab,ac) by defadd
.= a * (b + c) by Z2, B3, B9, B19, B20, defaddf ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

thus (b + c) * a = a * (b + c) by GROUP_1:def 12
.= (b * a) + (a * c) by I, GROUP_1:def 12
.= (b * a) + (c * a) by GROUP_1:def 12 ; :: thesis: verum

end;

end;

end;

hence embField f is distributive ; :: thesis: verum