let UN be Universe; for x being Element of RingObjects UN holds x is strict Ring
let x be Element of RingObjects UN; 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
; verum