let I be non empty set ; :: thesis: for G being Group
for H being Subgroup of G
for x being Function of I,G
for y being Function of I,H st x = y holds
support x = support y
let G be Group; :: thesis: for H being Subgroup of G
for x being Function of I,G
for y being Function of I,H st x = y holds
support x = support y
let H be Subgroup of G; :: thesis: for x being Function of I,G
for y being Function of I,H st x = y holds
support x = support y
let x be Function of I,G; :: thesis: for y being Function of I,H st x = y holds
support x = support y
let y be Function of I,H; :: thesis: ( x = y implies support x = support y )
assume A1: x = y ; :: thesis: support x = support y
for i being object holds
( i in support x iff i in support y )

proof

let i be object ; :: thesis: ( i in support x iff i in support y )
A2: ( i in support x iff ( x . i <> 1_ G & i in I ) ) by GROUP_19:def 2;
( i in support y iff ( y . i <> 1_ H & i in I ) ) by GROUP_19:def 2;
hence ( i in support x iff i in support y ) by A1, A2, GROUP_2:44; :: thesis: verum

end;

hence support x = support y by TARSKI:2; :: thesis: verum