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

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