let G be Group; :: thesis: for H being Subgroup of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
let H be Subgroup of G; :: thesis: for F being FinSequence of the carrier of G
for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
let F be FinSequence of the carrier of G; :: thesis: for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
let I be FinSequence of INT ; :: thesis: ( rng F c= carr H implies Product (F |^ I) in H )
assume A1: rng F c= carr H ; :: thesis: Product (F |^ I) in H
rng (F |^ I) c= carr H

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F |^ I) or x in carr H )
assume x in rng (F |^ I) ; :: thesis: x in carr H
then consider y being set such that
A2: ( y in dom (F |^ I) & x = (F |^ I) . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A2;
len (F |^ I) = len F by Def4;
then A3: y in dom F by A2, FINSEQ_3:31;
then A4: x = (F /. y) |^ (@ (I /. y)) by A2, Def4;
( F . y in rng F & F . y = F /. y ) by A3, FUNCT_1:def 5, PARTFUN1:def 8;
then F /. y in H by A1, STRUCT_0:def 5;
then x in H by A4, Th6;
hence x in carr H by STRUCT_0:def 5; :: thesis: verum

end;

hence Product (F |^ I) in H by Th21; :: thesis: verum