let n be non zero Nat; :: thesis: for i being Nat st i in dom (PrimeDivisorsFS n) holds
(PrimeDivisorsFS n) . i is prime
set f = PrimeDivisorsFS n;
let i be Nat; :: thesis: ( i in dom (PrimeDivisorsFS n) implies (PrimeDivisorsFS n) . i is prime )
assume i in dom (PrimeDivisorsFS n) ; :: thesis: (PrimeDivisorsFS n) . i is prime
then (PrimeDivisorsFS n) . i in rng (PrimeDivisorsFS n) by FUNCT_1:def 3;
then (PrimeDivisorsFS n) . i in PrimeDivisors n by FINSEQ_1:def 14;
then ex p being Prime st
( p = (PrimeDivisorsFS n) . i & p divides n ) ;
hence (PrimeDivisorsFS n) . i is prime ; :: thesis: verum