let I be set ; :: thesis: for F being Group-like associative multMagma-Family of I holds F is Group-yielding
let F be Group-like associative multMagma-Family of I; :: thesis: F is Group-yielding
let y be object ; :: according to GROUP_23:def 1 :: thesis: ( y in rng F implies y is Group )
assume y in rng F ; :: thesis: y is Group
then ex x being object st
( x in dom F & y = F . x ) by FUNCT_1:def 3;
hence y is Group by GROUP_19:1; :: thesis: verum