let n, m, k be Element of NAT ; :: thesis: ( PFArt n,m c= PFArt k,m implies n = k )
assume A1: PFArt n,m c= PFArt k,m ; :: thesis: n = k
assume n <> k ; :: thesis: contradiction
then 2 * n <> 2 * k ;
then A2: [(2 * n),m] <> [(2 * k),m] by ZFMISC_1:33;
[(2 * n),m] in PFArt n,m by Def2;
then ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [(2 * n),m] ) by A1, A2, Def2;
hence contradiction by ZFMISC_1:33; :: thesis: verum