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 )

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

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