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 object ; :: 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 object such that
A2: y in dom (F |^ I) and
A3: x = (F |^ I) . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A2;
len (F |^ I) = len F by Def3;
then A4: y in dom F by A2, FINSEQ_3:29;
then ( F . y in rng F & F . y = F /. y ) by FUNCT_1:def 3, PARTFUN1:def 6;
then A5: F /. y in H by A1, STRUCT_0:def 5;
x = (F /. y) |^ (@ (I /. y)) by A3, A4, Def3;
then x in H by A5, Th4;
hence x in carr H by STRUCT_0:def 5; :: thesis: verum
end;
hence Product (F |^ I) in H by Th18; :: thesis: verum