let A be non empty set ; :: thesis: for x, y, z being Element of (RAlgebra A)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RAlgebra A)) = x & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
let x, y, z be Element of (RAlgebra A); :: thesis: for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RAlgebra A)) = x & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
let a, b be Real; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RAlgebra A)) = x & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
reconsider f = x as Element of Funcs A,REAL ;
thus x + y = y + x by Th16; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. (RAlgebra A)) = x & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
thus (x + y) + z = x + (y + z) by Th17; :: thesis: ( x + (0. (RAlgebra A)) = x & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
thus x + (0. (RAlgebra A)) = (RealFuncAdd A) . (RealFuncZero A),f by Th16
.= x by Th21 ; :: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
thus x * y = y * x by Th18; :: thesis: ( (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
thus (x * y) * z = x * (y * z) by Th19; :: thesis: ( x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & 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) )
thus x * (1. (RAlgebra A)) = (RealFuncMult A) . (RealFuncUnit A),f by Th18
.= x by Th20 ; :: thesis: ( x * (y + z) = (x * y) + (x * z) & 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) )
thus x * (y + z) = (x * y) + (x * z) by Th26; :: 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) )
thus a * (x * y) = (a * x) * y by Th27; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus a * (x + y) = (a * x) + (a * y) by Lm2; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus (a + b) * x = (a * x) + (b * x) by Th25; :: thesis: (a * b) * x = a * (b * x)
thus (a * b) * x = a * (b * x) by Th24; :: thesis: verum