let I be non empty set ; :: thesis: for F being Group-Family of I
for F1, F2 being componentwise_strict Subgroup-Family of F st ( for i being Element of I holds Image (proj (F1,i)) is Subgroup of Image (proj (F2,i)) ) holds
product F1 is strict Subgroup of product F2
let F be Group-Family of I; :: thesis: for F1, F2 being componentwise_strict Subgroup-Family of F st ( for i being Element of I holds Image (proj (F1,i)) is Subgroup of Image (proj (F2,i)) ) holds
product F1 is strict Subgroup of product F2
let F1, F2 be componentwise_strict Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds Image (proj (F1,i)) is Subgroup of Image (proj (F2,i)) ) implies product F1 is strict Subgroup of product F2 )
assume A1: for i being Element of I holds Image (proj (F1,i)) is Subgroup of Image (proj (F2,i)) ; :: thesis: product F1 is strict Subgroup of product F2
for i being Element of I holds F1 . i is Subgroup of F2 . i

proof

let i be Element of I; :: thesis: F1 . i is Subgroup of F2 . i
Image (proj (F1,i)) is Subgroup of Image (proj (F2,i)) by A1;
hence F1 . i is Subgroup of F2 . i by Th50; :: thesis: verum

end;

hence product F1 is strict Subgroup of product F2 by Th49; :: thesis: verum