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 S₁[ 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 S₁[F] holds
S₁[F ^ <*d*>]

let F be FinSequence of the carrier of G; :: thesis: for d being Element of G st S₁[F] holds
S₁[F ^ <*d*>]
let d be Element of G; :: thesis: ( S₁[F] implies S₁[F ^ <*d*>] )
assume A2: S₁[F] ; :: thesis: S₁[F ^ <*d*>]
thus S₁[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: S₁[ <*> 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 S₁[F] from FINSEQ_2:sch 2(A6, A1);
hence ( rng F c= carr H implies Product F in H ) ; :: thesis: verum