let UN be Universe; :: thesis: for f being Morphism of (GroupCat UN)
for f' being Element of Morphs (GroupObjects UN)
for b being Object of (GroupCat UN)
for b' being Element of GroupObjects UN holds
( f is strict Element of Morphs (GroupObjects UN) & f' is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
set C = GroupCat UN;
set V = GroupObjects UN;
set X = Morphs (GroupObjects UN);
let f be Morphism of (GroupCat UN); :: thesis: for f' being Element of Morphs (GroupObjects UN)
for b being Object of (GroupCat UN)
for b' being Element of GroupObjects UN holds
( f is strict Element of Morphs (GroupObjects UN) & f' is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
let f' be Element of Morphs (GroupObjects UN); :: thesis: for b being Object of (GroupCat UN)
for b' being Element of GroupObjects UN holds
( f is strict Element of Morphs (GroupObjects UN) & f' is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
let b be Object of (GroupCat UN); :: thesis: for b' being Element of GroupObjects UN holds
( f is strict Element of Morphs (GroupObjects UN) & f' is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
let b' be Element of GroupObjects UN; :: thesis: ( f is strict Element of Morphs (GroupObjects UN) & f' is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
ex G, H being strict Element of GroupObjects UN st f is strict Morphism of G,H by Def30;
hence f is strict Element of Morphs (GroupObjects UN) ; :: thesis: ( f' is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
thus f' is Morphism of (GroupCat UN) ; :: thesis: ( b is strict Element of GroupObjects UN & b' is Object of (GroupCat UN) )
consider x being set such that
A1: ( x in UN & GO x,b ) by Def29;
ex x1, x2, x3, x4 being set st
( x = [x1,x2,x3,x4] & ex G being strict AddGroup st
( b = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ) by A1, Def28;
hence b is strict Element of GroupObjects UN ; :: thesis: b' is Object of (GroupCat UN)
thus b' is Object of (GroupCat UN) ; :: thesis: verum