let I be non empty set ; :: thesis: for G being Group

for H being Subgroup of G

for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

let G be Group; :: thesis: for H being Subgroup of G

for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

let H be Subgroup of G; :: thesis: for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

let x be finite-support Function of I,G; :: thesis: ( rng x c= [#] H implies x is finite-support Function of I,H )

assume rng x c= [#] H ; :: thesis: x is finite-support Function of I,H

then reconsider y = x as Function of I,H by FUNCT_2:6;

support x = support y by Th3;

hence x is finite-support Function of I,H by GROUP_19:def 3; :: thesis: verum

for H being Subgroup of G

for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

let G be Group; :: thesis: for H being Subgroup of G

for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

let H be Subgroup of G; :: thesis: for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

let x be finite-support Function of I,G; :: thesis: ( rng x c= [#] H implies x is finite-support Function of I,H )

assume rng x c= [#] H ; :: thesis: x is finite-support Function of I,H

then reconsider y = x as Function of I,H by FUNCT_2:6;

support x = support y by Th3;

hence x is finite-support Function of I,H by GROUP_19:def 3; :: thesis: verum