let I be non empty set ; 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; 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; 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; ( rng x c= [#] H implies x is finite-support Function of I,H )
assume
rng x c= [#] H
; 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; verum