let I be non empty set ; :: thesis: for G being Group
for a being Function of I,G st a = I --> (1_ G) holds
support a is empty
let G be Group; :: thesis: for a being Function of I,G st a = I --> (1_ G) holds
support a is empty
let a be Function of I,G; :: thesis: ( a = I --> (1_ G) implies support a is empty )
assume A1: a = I --> (1_ G) ; :: thesis: support a is empty
for i being object holds not i in support a

proof

let i be object ; :: thesis: not i in support a
assume A2: i in support a ; :: thesis: contradiction
then a . i = 1_ G by A1, FUNCOP_1:7;
hence contradiction by A2, Def2; :: thesis: verum

end;

hence support a is empty by XBOOLE_0:def 1; :: thesis: verum