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:
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 ; :: thesis: verum
end;
hence support x = support y by TARSKI:2; :: thesis: verum