set G = the trivial Group;
set f = I --> the trivial Group;
take I --> the trivial Group ; :: thesis: I --> the trivial Group is Group-yielding
let a be object ; :: according to GROUP_23:def 1 :: thesis: ( a in rng (I --> the trivial Group) implies a is Group )
assume a in rng (I --> the trivial Group) ; :: thesis: a is Group
then ex x being object st
( x in dom (I --> the trivial Group) & a = (I --> the trivial Group) . x ) by FUNCT_1:def 3;
hence a is Group by FUNCOP_1:7; :: thesis: verum