let I be non empty set ; :: thesis: for G being Group
for F being componentwise_strict Subgroup-Family of I,G holds F is Subgroups G -valued
let G be Group; :: thesis: for F being componentwise_strict Subgroup-Family of I,G holds F is Subgroups G -valued
let F be componentwise_strict Subgroup-Family of I,G; :: thesis: F is Subgroups G -valued
for y being object st y in rng F holds
y in Subgroups G

proof

let y be object ; :: thesis: ( y in rng F implies y in Subgroups G )
assume y in rng F ; :: thesis: y in Subgroups G
then consider i being Element of I such that
A1: y = F . i by MssRng;
y is strict Subgroup of G by A1, ThS2;
hence y in Subgroups G by GROUP_3:def 1; :: thesis: verum

end;

hence F is Subgroups G -valued by RELAT_1:def 19, TARSKI:def 3; :: thesis: verum