let X be RealNormSpace; :: thesis: for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X)

for a, b being Real holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: thesis: for a, b being Real holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

let a, b be Real; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

set RBLOP = R_Algebra_of_BoundedLinearOperators X;

set BLOP = BoundedLinearOperators (X,X);

set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));

set MULT = FuncMult X;

set UNIT = FuncUnit X;

set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);

reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;

thus x + y = f + g

.= y + x by RLVECT_1:2 ; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (x + y) + z = (f + g) + h

.= f + (g + h) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: ( x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))

.= x ; :: thesis: ( ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) :: thesis: ( (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4

.= (xx * yy) * zz by Def4

.= xx * (yy * zz) by Th7

.= (FuncMult X) . (xx,(yy * zz)) by Def4

.= x * (y * z) by Def4 ; :: thesis: ( x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4

.= x by Th8 ; :: thesis: ( (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (1. (R_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4

.= x by Th8 ; :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus x * (y + z) = xx * (yy + zz) by Def4

.= (xx * yy) + (xx * zz) by Th9

.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4

.= (x * y) + (x * z) by Def4 ; :: thesis: ( (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (y + z) * x = (yy + zz) * xx by Def4

.= (yy * xx) + (zz * xx) by Th10

.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4

.= (y * x) + (z * x) by Def4 ; :: thesis: ( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus a * (x * y) = a * (xx * yy) by Def4

.= (a * xx) * yy by Th12

.= (a * x) * y by Def4 ; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus a * (x + y) = a * (f + g)

.= (a * f) + (a * g) by RLVECT_1:def 5

.= (a * x) + (a * y) ; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (a + b) * x = (a + b) * f

.= (a * f) + (b * f) by RLVECT_1:def 6

.= (a * x) + (b * x) ; :: thesis: ( (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (a * b) * x = (a * b) * f

.= a * (b * f) by RLVECT_1:def 7

.= a * (b * x) ; :: thesis: (a * b) * (x * y) = (a * x) * (b * y)

thus (a * b) * (x * y) = (a * b) * (xx * yy) by Def4

.= (a * xx) * (b * yy) by Th11

.= (a * x) * (b * y) by Def4 ; :: thesis: verum

for a, b being Real holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: thesis: for a, b being Real holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

let a, b be Real; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

set RBLOP = R_Algebra_of_BoundedLinearOperators X;

set BLOP = BoundedLinearOperators (X,X);

set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));

set MULT = FuncMult X;

set UNIT = FuncUnit X;

set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);

reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;

thus x + y = f + g

.= y + x by RLVECT_1:2 ; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (x + y) + z = (f + g) + h

.= f + (g + h) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: ( x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))

.= x ; :: thesis: ( ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) :: thesis: ( (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

proof

reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that

A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def 11;

reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ;

take t ; :: thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X)

thus x + t = 0. (R_Algebra_of_BoundedLinearOperators X) by A1; :: thesis: verum

end;A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def 11;

reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ;

take t ; :: thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X)

thus x + t = 0. (R_Algebra_of_BoundedLinearOperators X) by A1; :: thesis: verum

thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4

.= (xx * yy) * zz by Def4

.= xx * (yy * zz) by Th7

.= (FuncMult X) . (xx,(yy * zz)) by Def4

.= x * (y * z) by Def4 ; :: thesis: ( x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4

.= x by Th8 ; :: thesis: ( (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (1. (R_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4

.= x by Th8 ; :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus x * (y + z) = xx * (yy + zz) by Def4

.= (xx * yy) + (xx * zz) by Th9

.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4

.= (x * y) + (x * z) by Def4 ; :: thesis: ( (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (y + z) * x = (yy + zz) * xx by Def4

.= (yy * xx) + (zz * xx) by Th10

.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4

.= (y * x) + (z * x) by Def4 ; :: thesis: ( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus a * (x * y) = a * (xx * yy) by Def4

.= (a * xx) * yy by Th12

.= (a * x) * y by Def4 ; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus a * (x + y) = a * (f + g)

.= (a * f) + (a * g) by RLVECT_1:def 5

.= (a * x) + (a * y) ; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (a + b) * x = (a + b) * f

.= (a * f) + (b * f) by RLVECT_1:def 6

.= (a * x) + (b * x) ; :: thesis: ( (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

thus (a * b) * x = (a * b) * f

.= a * (b * f) by RLVECT_1:def 7

.= a * (b * x) ; :: thesis: (a * b) * (x * y) = (a * x) * (b * y)

thus (a * b) * (x * y) = (a * b) * (xx * yy) by Def4

.= (a * xx) * (b * yy) by Th11

.= (a * x) * (b * y) by Def4 ; :: thesis: verum