let A be non empty set ; :: thesis: for x, y, z being Element of (RRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
let x, y, z be Element of (RRing A); :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
set IT = RRing A;
reconsider f = x as Element of Funcs (A,REAL) ;
thus x + y = y + x by Th5; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (x + y) + z = x + (y + z) by Th6; :: thesis: ( x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x + (0. (RRing A)) = (RealFuncAdd A) . ((RealFuncZero A),f) by Th5
.= x by Th10 ; :: thesis: ( ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus ex t being Element of (RRing A) st x + t = 0. (RRing A) :: thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

proof

set h = (RealFuncExtMult A) . [(- jj),f];
reconsider t = (RealFuncExtMult A) . [(- jj),f] as Element of (RRing A) ;
take t ; :: thesis: x + t = 0. (RRing A)
thus x + t = 0. (RRing A) by Th11; :: thesis: verum

end;

thus x * y = y * x by Th7; :: thesis: ( (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (x * y) * z = x * (y * z) by Th8; :: thesis: ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (1. (RRing A)) = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7
.= x by Th9 ; :: thesis: ( (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
hence (1. (RRing A)) * x = x by Th7; :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (y + z) = (x * y) + (x * z) by Th15; :: thesis: (y + z) * x = (y * x) + (z * x)
hence (y + z) * x = (x * y) + (x * z) by Th7
.= (y * x) + (x * z) by Th7
.= (y * x) + (z * x) by Th7 ;
:: thesis: verum