let UN be Universe; :: thesis: for x being Element of RingObjects UN holds x is strict Ring
let x be Element of RingObjects UN; :: thesis: x is strict Ring
consider u being set such that
u in UN and
A1: GO u,x by Def16;
ex x1, x2, x3, x4, x5, x6 being set st
( u = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) ) by A1;
hence x is strict Ring ; :: thesis: verum