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