let p be Nat; :: thesis: for fp being FinSequence of NAT

for a being Nat st a in dom fp & p divides fp . a holds

p divides Product fp

let fp be FinSequence of NAT ; :: thesis: for a being Nat st a in dom fp & p divides fp . a holds

p divides Product fp

let a be Nat; :: thesis: ( a in dom fp & p divides fp . a implies p divides Product fp )

assume that

A1: a in dom fp and

A2: p divides fp . a ; :: thesis: p divides Product fp

fp . a divides Product fp by A1, Th32;

hence p divides Product fp by A2, NAT_D:4; :: thesis: verum

for a being Nat st a in dom fp & p divides fp . a holds

p divides Product fp

let fp be FinSequence of NAT ; :: thesis: for a being Nat st a in dom fp & p divides fp . a holds

p divides Product fp

let a be Nat; :: thesis: ( a in dom fp & p divides fp . a implies p divides Product fp )

assume that

A1: a in dom fp and

A2: p divides fp . a ; :: thesis: p divides Product fp

fp . a divides Product fp by A1, Th32;

hence p divides Product fp by A2, NAT_D:4; :: thesis: verum