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