let G be Group; :: thesis: for H being Subgroup of G
for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H
let H be Subgroup of G; :: thesis: for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H
let F be FinSequence of the carrier of G; :: thesis: ( rng F c= carr H implies Product F in H )
defpred S1[ FinSequence of the carrier of G] means ( rng $1 c= carr H implies Product $1 in H );
A1: now :: thesis: for F being FinSequence of the carrier of G
for d being Element of G st S1[F] holds
S1[F ^ <*d*>]
let F be FinSequence of the carrier of G; :: thesis: for d being Element of G st S1[F] holds
S1[F ^ <*d*>]
let d be Element of G; :: thesis: ( S1[F] implies S1[F ^ <*d*>] )
assume A2: S1[F] ; :: thesis: S1[F ^ <*d*>]
thus S1[F ^ <*d*>] :: thesis: verum
proof
A3: ( rng F c= rng (F ^ <*d*>) & Product (F ^ <*d*>) = (Product F) * d ) by FINSEQ_1:29, FINSOP_1:4;
A4: ( rng <*d*> = {d} & d in {d} ) by FINSEQ_1:39, TARSKI:def 1;
assume A5: rng (F ^ <*d*>) c= carr H ; :: thesis: Product (F ^ <*d*>) in H
rng <*d*> c= rng (F ^ <*d*>) by FINSEQ_1:30;
then rng <*d*> c= carr H by A5;
then d in H by A4, STRUCT_0:def 5;
hence Product (F ^ <*d*>) in H by A2, A5, A3, GROUP_2:50, XBOOLE_1:1; :: thesis: verum
end;
end;
A6: S1[ <*> the carrier of G]
proof
assume rng (<*> the carrier of G) c= carr H ; :: thesis: Product (<*> the carrier of G) in H
1_ G in H by GROUP_2:46;
hence Product (<*> the carrier of G) in H by Th8; :: thesis: verum
end;
for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch 2(A6, A1);
 hence ( rng F c= carr H implies Product F in H ) ; :: thesis: verum