let I be non empty set ; :: thesis: for G being Group
for H being Subgroup of G
for y being finite-support Function of I,H holds y is finite-support Function of I,G
let G be Group; :: thesis: for H being Subgroup of G
for y being finite-support Function of I,H holds y is finite-support Function of I,G
let H be Subgroup of G; :: thesis: for y being finite-support Function of I,H holds y is finite-support Function of I,G
let y be finite-support Function of I,H; :: thesis: y is finite-support Function of I,G
[#] H c= [#] G by GROUP_2:def 5;
then reconsider x = y as Function of I,G by FUNCT_2:7;
support x = support y by Th3;
hence y is finite-support Function of I,G by GROUP_19:def 3; :: thesis: verum