let f, F be Function of NAT ,NAT ; :: thesis: ( f is multiplicative & ( for n0 being non zero natural number holds F . n0 = Sum (f | (NatDivisors n0)) ) implies F is multiplicative )
assume A1: f is multiplicative ; :: thesis: ( ex n0 being non zero natural number st not F . n0 = Sum (f | (NatDivisors n0)) or F is multiplicative )
assume A2: for n0 being non zero natural number holds F . n0 = Sum (f | (NatDivisors n0)) ; :: thesis: F is multiplicative
for n, m being non zero natural number st n,m are_relative_prime holds
F . (n * m) = (F . n) * (F . m)

proof

let n, m be non zero natural number ; :: thesis: ( n,m are_relative_prime implies F . (n * m) = (F . n) * (F . m) )
assume A3: n,m are_relative_prime ; :: thesis: F . (n * m) = (F . n) * (F . m)
set b1 = f | (NatDivisors (n * m));
set b2 = (multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):];
consider f1 being FinSequence of REAL such that
A4: ( Sum (f | (NatDivisors (n * m))) = Sum f1 & f1 = (f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m))))) ) by UPROOTS:def 3;
consider f2 being FinSequence of REAL such that
A5: ( Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) = Sum f2 & f2 = ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ) by UPROOTS:def 3;
set g1 = canFS (support (f | (NatDivisors (n * m))));
set g2 = canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]));
set h' = multnat | [:(NatDivisors n),(NatDivisors m):];
dom multnat = [:NAT ,NAT :] by FUNCT_2:def 1;
then A6: dom (multnat | [:(NatDivisors n),(NatDivisors m):]) = [:(NatDivisors n),(NatDivisors m):] by RELAT_1:91;
A7: dom [:f,f:] = [:NAT ,NAT :] by FUNCT_2:def 1;
dom (multnat * [:f,f:]) = [:NAT ,NAT :] by FUNCT_2:def 1;
then A8: dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) = [:(NatDivisors n),(NatDivisors m):] by RELAT_1:91;
dom f = NAT by FUNCT_2:def 1;
then A9: dom (f | (NatDivisors (n * m))) = NatDivisors (n * m) by RELAT_1:91;
for x1, x2 being set st x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) & (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 implies x1 = x2 )
assume A10: x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) ; :: thesis: ( not x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) or not (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 or x1 = x2 )
then consider n1, m1 being set such that
A11: ( n1 in NatDivisors n & m1 in NatDivisors m & x1 = [n1,m1] ) by A6, ZFMISC_1:def 2;
reconsider n1 = n1, m1 = m1 as Element of NAT by A11;
assume A12: x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):]) ; :: thesis: ( not (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 or x1 = x2 )
then consider n2, m2 being set such that
A13: ( n2 in NatDivisors n & m2 in NatDivisors m & x2 = [n2,m2] ) by A6, ZFMISC_1:def 2;
reconsider n2 = n2, m2 = m2 as Element of NAT by A13;
assume A14: (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 ; :: thesis: x1 = x2
A15: (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = multnat . x1 by A10, FUNCT_1:70
.= multnat . n1,m1 by A11, BINOP_1:def 1
.= n1 * m1 by BINOP_2:def 24 ;
(multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 = multnat . x2 by A12, FUNCT_1:70
.= multnat . n2,m2 by A13, BINOP_1:def 1
.= n2 * m2 by BINOP_2:def 24 ;
then ( n1 = n2 & m1 = m2 ) by A11, A13, A3, A15, A14, Th15;
hence x1 = x2 by A11, A13; :: thesis: verum

end;

then reconsider h' = multnat | [:(NatDivisors n),(NatDivisors m):] as one-to-one Function by FUNCT_1:def 8;
set h = (((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])));
A16: dom ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f2

proof

A17: support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by POLYNOM1:41;
for x being set st x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) holds
x in dom (((canFS (support (f | (NatDivisors (n * m))))) " ) * h')

proof

let x be set ; :: thesis: ( x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) implies x in dom (((canFS (support (f | (NatDivisors (n * m))))) " ) * h') )
assume A18: x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) ; :: thesis: x in dom (((canFS (support (f | (NatDivisors (n * m))))) " ) * h')
then A19: ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x <> 0 by POLYNOM1:def 7;
A20: x in [:(NatDivisors n),(NatDivisors m):] by A8, A18, A17;
consider n1, m1 being set such that
A21: ( n1 in NatDivisors n & m1 in NatDivisors m & x = [n1,m1] ) by A8, A18, A17, ZFMISC_1:def 2;
reconsider n1 = n1, m1 = m1 as Element of NAT by A21;
reconsider n1' = n1, m1' = m1 as non zero natural number by A21, MOEBIUS1:39;
set x' = ((canFS (support (f | (NatDivisors (n * m))))) " ) . (n1 * m1);
A22: rng (canFS (support (f | (NatDivisors (n * m))))) = support (f | (NatDivisors (n * m))) by FUNCT_2:def 3;
set fn1 = f . n1;
set fm1 = f . m1;
A23: n1,m1 are_relative_prime by Th14, A21, A3;
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x = (multnat * [:f,f:]) . x by A8, A18, A17, FUNCT_1:72
.= multnat . ([:f,f:] . x) by A7, A20, FUNCT_1:23
.= multnat . ([:f,f:] . n1,m1) by A21, BINOP_1:def 1
.= multnat . [(f . n1),(f . m1)] by FUNCT_3:96
.= multnat . (f . n1),(f . m1) by BINOP_1:def 1
.= (f . n1) * (f . m1) by BINOP_2:def 24
.= f . (n1' * m1') by A23, A1, Def5
.= (f | (NatDivisors (n * m))) . (n1 * m1) by A21, Th16, FUNCT_1:72 ;
then A24: n1 * m1 in rng (canFS (support (f | (NatDivisors (n * m))))) by A22, A19, POLYNOM1:def 7;
then n1 * m1 in dom ((canFS (support (f | (NatDivisors (n * m))))) " ) by FUNCT_1:55;
then ((canFS (support (f | (NatDivisors (n * m))))) " ) . (n1 * m1) in rng ((canFS (support (f | (NatDivisors (n * m))))) " ) by FUNCT_1:12;
then A25: ((canFS (support (f | (NatDivisors (n * m))))) " ) . (n1 * m1) in dom (canFS (support (f | (NatDivisors (n * m))))) by FUNCT_1:55;
(canFS (support (f | (NatDivisors (n * m))))) . (((canFS (support (f | (NatDivisors (n * m))))) " ) . (n1 * m1)) = n1 * m1 by A24, FUNCT_1:57
.= multnat . n1,m1 by BINOP_2:def 24
.= multnat . [n1,m1] by BINOP_1:def 1
.= h' . x by A21, A8, A18, A17, FUNCT_1:72 ;
then h' . x in rng (canFS (support (f | (NatDivisors (n * m))))) by A25, FUNCT_1:def 5;
then h' . x in dom ((canFS (support (f | (NatDivisors (n * m))))) " ) by FUNCT_1:55;
hence x in dom (((canFS (support (f | (NatDivisors (n * m))))) " ) * h') by A6, A8, A18, A17, FUNCT_1:21; :: thesis: verum

end;

then support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom (((canFS (support (f | (NatDivisors (n * m))))) " ) * h') by TARSKI:def 3;
then rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom (((canFS (support (f | (NatDivisors (n * m))))) " ) * h') by FUNCT_2:def 3;
then A26: dom ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by RELAT_1:46;
rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by A17, FUNCT_2:def 3;
hence dom ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f2 by A5, A26, RELAT_1:46; :: thesis: verum

end;

A27: rng ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f1

proof

A28: support (f | (NatDivisors (n * m))) c= dom (f | (NatDivisors (n * m))) by POLYNOM1:41;
rng (canFS (support (f | (NatDivisors (n * m))))) c= dom (f | (NatDivisors (n * m))) by A28, FUNCT_2:def 3;
then A29: dom ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) = dom (canFS (support (f | (NatDivisors (n * m))))) by RELAT_1:46;
for y being set st y in rng (canFS (support (f | (NatDivisors (n * m))))) holds
y in rng (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))

proof

let y be set ; :: thesis: ( y in rng (canFS (support (f | (NatDivisors (n * m))))) implies y in rng (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) )
assume A30: y in rng (canFS (support (f | (NatDivisors (n * m))))) ; :: thesis: y in rng (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
then A31: y in support (f | (NatDivisors (n * m))) ;
A32: (f | (NatDivisors (n * m))) . y <> 0 by A30, POLYNOM1:def 7;
A33: support (f | (NatDivisors (n * m))) c= dom (f | (NatDivisors (n * m))) by POLYNOM1:41;
consider n1, m1 being natural number such that
A34: ( n1 in NatDivisors n & m1 in NatDivisors m & y = n1 * m1 ) by A33, Th18, A3, A9, A31;
reconsider n1' = n1, m1' = m1 as non zero natural number by A34, MOEBIUS1:39;
reconsider n1 = n1, m1 = m1 as Element of NAT by ORDINAL1:def 13;
set x = ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1];
A35: n1,m1 are_relative_prime by Th14, A34, A3;
set fn1 = f . n1;
set fm1 = f . m1;
A36: [n1,m1] in [:(NatDivisors n),(NatDivisors m):] by A34, ZFMISC_1:def 2;
A37: [n1,m1] in [:(NatDivisors n),(NatDivisors m):] by A34, ZFMISC_1:def 2;
(f | (NatDivisors (n * m))) . y = f . y by A33, A9, A31, FUNCT_1:72
.= (f . n1') * (f . m1') by A34, A35, A1, Def5
.= multnat . (f . n1),(f . m1) by BINOP_2:def 24
.= multnat . [(f . n1),(f . m1)] by BINOP_1:def 1
.= multnat . ([:f,f:] . n1,m1) by FUNCT_3:96
.= multnat . ([:f,f:] . [n1,m1]) by BINOP_1:def 1
.= (multnat * [:f,f:]) . [n1,m1] by A7, FUNCT_1:23
.= ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1] by A37, FUNCT_1:72 ;
then [n1,m1] in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by A32, POLYNOM1:def 7;
then A38: [n1,m1] in rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by FUNCT_2:def 3;
then [n1,m1] in dom ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) by FUNCT_1:55;
then ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1] in rng ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) by FUNCT_1:12;
then A39: ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1] in dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by FUNCT_1:55;
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1]) = [n1,m1] by A38, FUNCT_1:57;
then A40: ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1] in dom (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by A39, A36, A6, FUNCT_1:21;
y = multnat . n1,m1 by A34, BINOP_2:def 24
.= multnat . [n1,m1] by BINOP_1:def 1
.= (multnat | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1] by A36, FUNCT_1:72
.= h' . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1])) by A38, FUNCT_1:57
.= (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) " ) . [n1,m1]) by A39, FUNCT_1:23 ;
hence y in rng (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by A40, FUNCT_1:def 5; :: thesis: verum

end;

then rng (canFS (support (f | (NatDivisors (n * m))))) c= rng (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by TARSKI:def 3;
then dom ((canFS (support (f | (NatDivisors (n * m))))) " ) c= rng (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by FUNCT_1:55;
then rng (((canFS (support (f | (NatDivisors (n * m))))) " ) * (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) = rng ((canFS (support (f | (NatDivisors (n * m))))) " ) by RELAT_1:47;
then rng (((canFS (support (f | (NatDivisors (n * m))))) " ) * (h' * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) = dom (canFS (support (f | (NatDivisors (n * m))))) by FUNCT_1:55;
hence rng ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f1 by A4, A29, RELAT_1:55; :: thesis: verum

end;

A41: for x being set holds
( x in dom f2 iff ( x in dom ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) & ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x in dom f1 ) ) by A16, A27, FUNCT_1:12;
A42: for x being set st x in dom f2 holds
f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x)

proof

let x be set ; :: thesis: ( x in dom f2 implies f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) )
assume A43: x in dom f2 ; :: thesis: f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x)
then A44: ( x in dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) & (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) ) by A5, FUNCT_1:21;
A45: ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) . (((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) = (((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) . x by FUNCT_1:23, A43, A16
.= ((((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) " ) * h')) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x by RELAT_1:55
.= (((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) " ) * h')) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A44, FUNCT_1:23 ;
set x' = (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x;
A46: support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by POLYNOM1:41;
A47: (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) by A44, FUNCT_1:12;
then A48: (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) ;
A49: (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in [:(NatDivisors n),(NatDivisors m):] by A48, A46, A8;
consider n1, m1 being set such that
A50: ( n1 in NatDivisors n & m1 in NatDivisors m & (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x = [n1,m1] ) by A48, A46, A8, ZFMISC_1:def 2;
reconsider n1 = n1, m1 = m1 as Element of NAT by A50;
reconsider n1' = n1, m1' = m1 as non zero natural number by A50, MOEBIUS1:39;
set fn1 = f . n1;
set fm1 = f . m1;
A51: n1,m1 are_relative_prime by Th14, A50, A3;
A52: ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) " ) * h') = (((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * ((canFS (support (f | (NatDivisors (n * m))))) " )) * h' by RELAT_1:55
.= ((f | (NatDivisors (n * m))) * ((canFS (support (f | (NatDivisors (n * m))))) * ((canFS (support (f | (NatDivisors (n * m))))) " ))) * h' by RELAT_1:55
.= ((f | (NatDivisors (n * m))) * (id (rng (canFS (support (f | (NatDivisors (n * m)))))))) * h' by FUNCT_1:61
.= ((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) * h' by FUNCT_2:def 3 ;
A53: ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) <> 0 by A47, POLYNOM1:def 7;
A54: ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) = (multnat * [:f,f:]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A48, A46, A8, FUNCT_1:72
.= multnat . ([:f,f:] . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)) by A7, A49, FUNCT_1:23
.= multnat . ([:f,f:] . n1,m1) by A50, BINOP_1:def 1
.= multnat . [(f . n1),(f . m1)] by FUNCT_3:96
.= multnat . (f . n1),(f . m1) by BINOP_1:def 1
.= (f . n1) * (f . m1) by BINOP_2:def 24
.= f . (n1' * m1') by A51, A1, Def5 ;
f . (n1' * m1') = (f | (NatDivisors (n * m))) . (n1 * m1) by A50, Th16, FUNCT_1:72;
then A55: n1 * m1 in support (f | (NatDivisors (n * m))) by A53, A54, POLYNOM1:def 7;
then A56: n1 * m1 in dom (id (support (f | (NatDivisors (n * m))))) by RELAT_1:71;
A57: h' . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) = multnat . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A48, A46, A6, A8, FUNCT_1:70
.= multnat . n1,m1 by A50, BINOP_1:def 1
.= n1 * m1 by BINOP_2:def 24 ;
(((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) * h') . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) = ((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) . (h' . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)) by A48, A46, A6, A8, FUNCT_1:23
.= (f | (NatDivisors (n * m))) . ((id (support (f | (NatDivisors (n * m))))) . (n1 * m1)) by A57, A56, FUNCT_1:23
.= (f | (NatDivisors (n * m))) . (n1 * m1) by A55, FUNCT_1:35
.= ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) by A54, A50, Th16, FUNCT_1:72 ;
hence f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) by A4, A5, A44, A45, A52, FUNCT_1:23; :: thesis: verum

end;

f2 = f1 * ((((canFS (support (f | (NatDivisors (n * m))))) " ) * h') * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) by A41, A42, FUNCT_1:20;
then A58: f1,f2 are_fiberwise_equipotent by A16, A27, CLASSES1:85;
thus F . (n * m) = Sum (f | (NatDivisors (n * m))) by A2
.= Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) by A4, A5, A58, RFINSEQ:22
.= (Sum (f | (NatDivisors n))) * (Sum (f | (NatDivisors m))) by Th28
.= (Sum (f | (NatDivisors n))) * (F . m) by A2
.= (F . n) * (F . m) by A2 ; :: thesis: verum

end;

hence F is multiplicative by Def5; :: thesis: verum