let n, m be non zero Nat; :: thesis: ( n,m are_coprime implies rng (pfexp (n * m)) = (rng (pfexp n)) \/ (rng (pfexp m)) )
assume A1: n,m are_coprime ; :: thesis: rng (pfexp (n * m)) = (rng (pfexp n)) \/ (rng (pfexp m))
A2: pfexp (n * m) = (pfexp n) + (pfexp m) by NAT_3:49;
A3: support (pfexp (n * m)) = (support (pfexp n)) \/ (support (pfexp m)) by NAT_3:46;
A4: rng (pfexp (n * m)) c= (rng (pfexp n)) \/ (rng (pfexp m))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pfexp (n * m)) or y in (rng (pfexp n)) \/ (rng (pfexp m)) )
assume A5: y in rng (pfexp (n * m)) ; :: thesis: y in (rng (pfexp n)) \/ (rng (pfexp m))
consider x being object such that
A6: ( x in dom (pfexp (n * m)) & (pfexp (n * m)) . x = y ) by A5, FUNCT_1:def 3;
A7: (pfexp (n * m)) . x = ((pfexp n) . x) + ((pfexp m) . x) by A2, PRE_POLY:def 5;

per cases ( not x in support (pfexp (n * m)) or x in support (pfexp n) or x in support (pfexp m) ) by A3, XBOOLE_0:def 3;

suppose not x in support (pfexp (n * m)) ; :: thesis: y in (rng (pfexp n)) \/ (rng (pfexp m))

then A8: (pfexp (n * m)) . x = 0 by PRE_POLY:def 7;
0 in rng (pfexp n) by Th23;
hence y in (rng (pfexp n)) \/ (rng (pfexp m)) by A6, A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in support (pfexp n) ; :: thesis: y in (rng (pfexp n)) \/ (rng (pfexp m))

then not x in support (pfexp m) by A1, NAT_3:44, XBOOLE_0:3;
then (pfexp m) . x = 0 by PRE_POLY:def 7;
then ( (pfexp (n * m)) . x = (pfexp n) . x & dom (pfexp n) = SetPrimes ) by A7, PARTFUN1:def 2;
then (pfexp (n * m)) . x in rng (pfexp n) by A6, FUNCT_1:def 3;
hence y in (rng (pfexp n)) \/ (rng (pfexp m)) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in support (pfexp m) ; :: thesis: y in (rng (pfexp n)) \/ (rng (pfexp m))

then not x in support (pfexp n) by A1, NAT_3:44, XBOOLE_0:3;
then (pfexp n) . x = 0 by PRE_POLY:def 7;
then ( (pfexp (n * m)) . x = (pfexp m) . x & dom (pfexp m) = SetPrimes ) by A7, PARTFUN1:def 2;
then (pfexp (n * m)) . x in rng (pfexp m) by A6, FUNCT_1:def 3;
hence y in (rng (pfexp n)) \/ (rng (pfexp m)) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A9: rng (pfexp n) c= rng (pfexp (n * m))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pfexp n) or y in rng (pfexp (n * m)) )
assume A10: y in rng (pfexp n) ; :: thesis: y in rng (pfexp (n * m))
consider x being object such that
A11: ( x in dom (pfexp n) & (pfexp n) . x = y ) by A10, FUNCT_1:def 3;
A12: ( dom (pfexp (n * m)) = SetPrimes & SetPrimes = dom (pfexp n) ) by PARTFUN1:def 2;
A13: (pfexp (n * m)) . x = ((pfexp n) . x) + ((pfexp m) . x) by A2, PRE_POLY:def 5;

per cases ( not x in support (pfexp n) or x in support (pfexp n) ) ;

suppose not x in support (pfexp n) ; :: thesis: y in rng (pfexp (n * m))

then (pfexp n) . x = 0 by PRE_POLY:def 7;
hence y in rng (pfexp (n * m)) by A11, Th23; :: thesis: verum

end;

suppose x in support (pfexp n) ; :: thesis: y in rng (pfexp (n * m))

then not x in support (pfexp m) by A1, NAT_3:44, XBOOLE_0:3;
then (pfexp m) . x = 0 by PRE_POLY:def 7;
hence y in rng (pfexp (n * m)) by A11, A13, A12, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

rng (pfexp m) c= rng (pfexp (n * m))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pfexp m) or y in rng (pfexp (n * m)) )
assume A14: y in rng (pfexp m) ; :: thesis: y in rng (pfexp (n * m))
consider x being object such that
A15: ( x in dom (pfexp m) & (pfexp m) . x = y ) by A14, FUNCT_1:def 3;
A16: ( dom (pfexp (n * m)) = SetPrimes & SetPrimes = dom (pfexp m) ) by PARTFUN1:def 2;
A17: (pfexp (n * m)) . x = ((pfexp n) . x) + ((pfexp m) . x) by A2, PRE_POLY:def 5;

per cases ( not x in support (pfexp m) or x in support (pfexp m) ) ;

suppose not x in support (pfexp m) ; :: thesis: y in rng (pfexp (n * m))

then (pfexp m) . x = 0 by PRE_POLY:def 7;
hence y in rng (pfexp (n * m)) by A15, Th23; :: thesis: verum

end;

suppose x in support (pfexp m) ; :: thesis: y in rng (pfexp (n * m))

then not x in support (pfexp n) by A1, NAT_3:44, XBOOLE_0:3;
then (pfexp n) . x = 0 by PRE_POLY:def 7;
hence y in rng (pfexp (n * m)) by A15, A17, A16, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then (rng (pfexp n)) \/ (rng (pfexp m)) c= rng (pfexp (n * m)) by A9, XBOOLE_1:8;
hence rng (pfexp (n * m)) = (rng (pfexp n)) \/ (rng (pfexp m)) by A4, XBOOLE_0:def 10; :: thesis: verum