let f, F be Function of NAT,NAT; ( f is multiplicative & ( for n0 being natural non zero number holds F . n0 = Sum (f | (NatDivisors n0)) ) implies F is multiplicative )
assume A1:
f is multiplicative
; ( ex n0 being natural non zero number st not F . n0 = Sum (f | (NatDivisors n0)) or F is multiplicative )
assume A2:
for n0 being natural non zero number holds F . n0 = Sum (f | (NatDivisors n0))
; F is multiplicative
for n, m being natural non zero number st n,m are_relative_prime holds
F . (n * m) = (F . n) * (F . m)
proof
let n,
m be
natural non
zero number ;
( n,m are_relative_prime implies 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 A3:
Sum (f | (NatDivisors (n * m))) = Sum f1
and A4:
f1 = (f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))
by UPROOTS:def 3;
set h9 =
multnat | [:(NatDivisors n),(NatDivisors m):];
set g2 =
canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]));
set g1 =
canFS (support (f | (NatDivisors (n * m))));
consider f2 being
FinSequence of
REAL such that A5:
Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) = Sum f2
and A6:
f2 = ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))
by UPROOTS:def 3;
dom multnat = [:NAT,NAT:]
by FUNCT_2:def 1;
then A7:
dom (multnat | [:(NatDivisors n),(NatDivisors m):]) = [:(NatDivisors n),(NatDivisors m):]
by RELAT_1:62;
assume A8:
n,
m are_relative_prime
;
F . (n * m) = (F . n) * (F . m)
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 ;
( 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 A9:
x1 in dom (multnat | [:(NatDivisors n),(NatDivisors m):])
;
( 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 A10:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A11:
x1 = [n1,m1]
by A7, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by A10;
A12:
(multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 =
multnat . x1
by A9, FUNCT_1:47
.=
multnat . (
n1,
m1)
by A11, BINOP_1:def 1
.=
n1 * m1
by BINOP_2:def 24
;
assume A13:
x2 in dom (multnat | [:(NatDivisors n),(NatDivisors m):])
;
( not (multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 or x1 = x2 )
then consider n2,
m2 being
set such that A14:
n2 in NatDivisors n
and A15:
m2 in NatDivisors m
and A16:
x2 = [n2,m2]
by A7, ZFMISC_1:def 2;
reconsider n2 =
n2,
m2 =
m2 as
Element of
NAT by A14, A15;
assume A17:
(multnat | [:(NatDivisors n),(NatDivisors m):]) . x1 = (multnat | [:(NatDivisors n),(NatDivisors m):]) . x2
;
x1 = x2
A18:
(multnat | [:(NatDivisors n),(NatDivisors m):]) . x2 =
multnat . x2
by A13, FUNCT_1:47
.=
multnat . (
n2,
m2)
by A16, BINOP_1:def 1
.=
n2 * m2
by BINOP_2:def 24
;
then
n1 = n2
by A8, A10, A14, A15, A17, A12, Th15;
hence
x1 = x2
by A8, A10, A11, A15, A16, A17, A12, A18, Th15;
verum
end;
then reconsider h9 =
multnat | [:(NatDivisors n),(NatDivisors m):] as
one-to-one Function by FUNCT_1:def 4;
set h =
(((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])));
A19:
support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
by PRE_POLY:37;
dom (multnat * [:f,f:]) = [:NAT,NAT:]
by FUNCT_2:def 1;
then A20:
dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) = [:(NatDivisors n),(NatDivisors m):]
by RELAT_1:62;
A21:
dom [:f,f:] = [:NAT,NAT:]
by FUNCT_2:def 1;
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))))) ") * h9)
proof
let x be
set ;
( x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) implies x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) )
A22:
rng (canFS (support (f | (NatDivisors (n * m))))) = support (f | (NatDivisors (n * m)))
by FUNCT_2:def 3;
assume A23:
x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
;
x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
then A24:
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x <> 0
by PRE_POLY:def 7;
A25:
x in [:(NatDivisors n),(NatDivisors m):]
by A20, A19, A23;
consider n1,
m1 being
set such that A26:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A27:
x = [n1,m1]
by A20, A19, A23, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by A26;
A28:
n1,
m1 are_relative_prime
by A8, A26, Th14;
reconsider n19 =
n1,
m19 =
m1 as
natural non
zero number by A26, MOEBIUS1:39;
set x9 =
((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1);
set fn1 =
f . n1;
set fm1 =
f . m1;
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x =
(multnat * [:f,f:]) . x
by A20, A19, A23, FUNCT_1:49
.=
multnat . ([:f,f:] . x)
by A21, A25, FUNCT_1:13
.=
multnat . ([:f,f:] . (n1,m1))
by A27, BINOP_1:def 1
.=
multnat . [(f . n1),(f . m1)]
by FUNCT_3:75
.=
multnat . (
(f . n1),
(f . m1))
by BINOP_1:def 1
.=
(f . n1) * (f . m1)
by BINOP_2:def 24
.=
f . (n19 * m19)
by A1, A28, Def5
.=
(f | (NatDivisors (n * m))) . (n1 * m1)
by A26, Th16, FUNCT_1:49
;
then A29:
n1 * m1 in rng (canFS (support (f | (NatDivisors (n * m)))))
by A24, A22, PRE_POLY:def 7;
then
n1 * m1 in dom ((canFS (support (f | (NatDivisors (n * m))))) ")
by FUNCT_1:33;
then
((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1) in rng ((canFS (support (f | (NatDivisors (n * m))))) ")
by FUNCT_1:3;
then A30:
((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1) in dom (canFS (support (f | (NatDivisors (n * m)))))
by FUNCT_1:33;
(canFS (support (f | (NatDivisors (n * m))))) . (((canFS (support (f | (NatDivisors (n * m))))) ") . (n1 * m1)) =
n1 * m1
by A29, FUNCT_1:35
.=
multnat . (
n1,
m1)
by BINOP_2:def 24
.=
multnat . [n1,m1]
by BINOP_1:def 1
.=
h9 . x
by A20, A19, A23, A27, FUNCT_1:49
;
then
h9 . x in rng (canFS (support (f | (NatDivisors (n * m)))))
by A30, FUNCT_1:def 3;
then
h9 . x in dom ((canFS (support (f | (NatDivisors (n * m))))) ")
by FUNCT_1:33;
hence
x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
by A7, A20, A19, A23, FUNCT_1:11;
verum
end;
then
support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
by TARSKI:def 3;
then
rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
by FUNCT_2:def 3;
then A31:
dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))
by RELAT_1:27;
rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
by A19, FUNCT_2:def 3;
then A32:
dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f2
by A6, A31, RELAT_1:27;
A33:
for
x being
set st
x in dom f2 holds
f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x)
proof
let x be
set ;
( x in dom f2 implies f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x) )
set x9 =
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x;
A34:
((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) =
(((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * ((canFS (support (f | (NatDivisors (n * m))))) ")) * h9
by RELAT_1:36
.=
((f | (NatDivisors (n * m))) * ((canFS (support (f | (NatDivisors (n * m))))) * ((canFS (support (f | (NatDivisors (n * m))))) "))) * h9
by RELAT_1:36
.=
((f | (NatDivisors (n * m))) * (id (rng (canFS (support (f | (NatDivisors (n * m)))))))) * h9
by FUNCT_1:39
.=
((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) * h9
by FUNCT_2:def 3
;
assume A35:
x in dom f2
;
f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x)
then A36:
x in dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))
by A6, FUNCT_1:11;
then A37:
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))
by FUNCT_1:3;
then A38:
(
support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) &
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) )
by PRE_POLY:37;
then consider n1,
m1 being
set such that A39:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A40:
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x = [n1,m1]
by A20, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by A39;
A41:
n1,
m1 are_relative_prime
by A8, A39, Th14;
reconsider n19 =
n1,
m19 =
m1 as
natural non
zero number by A39, MOEBIUS1:39;
set fn1 =
f . n1;
set fm1 =
f . m1;
A42:
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in [:(NatDivisors n),(NatDivisors m):]
by A20, A38;
A43:
((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 A20, A38, FUNCT_1:49
.=
multnat . ([:f,f:] . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x))
by A21, A42, FUNCT_1:13
.=
multnat . ([:f,f:] . (n1,m1))
by A40, BINOP_1:def 1
.=
multnat . [(f . n1),(f . m1)]
by FUNCT_3:75
.=
multnat . (
(f . n1),
(f . m1))
by BINOP_1:def 1
.=
(f . n1) * (f . m1)
by BINOP_2:def 24
.=
f . (n19 * m19)
by A1, A41, Def5
;
A44:
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) <> 0
by A37, PRE_POLY:def 7;
f . (n19 * m19) = (f | (NatDivisors (n * m))) . (n1 * m1)
by A39, Th16, FUNCT_1:49;
then A45:
n1 * m1 in support (f | (NatDivisors (n * m)))
by A44, A43, PRE_POLY:def 7;
then A46:
n1 * m1 in dom (id (support (f | (NatDivisors (n * m)))))
by RELAT_1:45;
A47:
h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) =
multnat . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)
by A7, A20, A38, FUNCT_1:47
.=
multnat . (
n1,
m1)
by A40, BINOP_1:def 1
.=
n1 * m1
by BINOP_2:def 24
;
A48:
((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (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))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) . x
by A32, A35, FUNCT_1:13
.=
((((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x
by RELAT_1:36
.=
(((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) * (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)
by A36, FUNCT_1:13
;
(((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) * h9) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) =
((f | (NatDivisors (n * m))) * (id (support (f | (NatDivisors (n * m)))))) . (h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x))
by A7, A20, A38, FUNCT_1:13
.=
(f | (NatDivisors (n * m))) . ((id (support (f | (NatDivisors (n * m))))) . (n1 * m1))
by A46, A47, FUNCT_1:13
.=
(f | (NatDivisors (n * m))) . (n1 * m1)
by A45, FUNCT_1:18
.=
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)
by A39, A43, Th16, FUNCT_1:49
;
hence
f2 . x = f1 . (((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x)
by A4, A6, A36, A48, A34, FUNCT_1:13;
verum
end;
dom f = NAT
by FUNCT_2:def 1;
then A49:
dom (f | (NatDivisors (n * m))) = NatDivisors (n * m)
by RELAT_1:62;
for
y being
set st
y in rng (canFS (support (f | (NatDivisors (n * m))))) holds
y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
proof
let y be
set ;
( y in rng (canFS (support (f | (NatDivisors (n * m))))) implies y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) )
assume A50:
y in rng (canFS (support (f | (NatDivisors (n * m)))))
;
y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
then A51:
y in support (f | (NatDivisors (n * m)))
;
A52:
support (f | (NatDivisors (n * m))) c= dom (f | (NatDivisors (n * m)))
by PRE_POLY:37;
then consider n1,
m1 being
natural number such that A53:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A54:
y = n1 * m1
by A8, A49, A51, Th18;
reconsider n19 =
n1,
m19 =
m1 as
natural non
zero number by A53, MOEBIUS1:39;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by ORDINAL1:def 12;
A55:
n1,
m1 are_relative_prime
by A8, A53, Th14;
A56:
(f | (NatDivisors (n * m))) . y <> 0
by A50, PRE_POLY:def 7;
A57:
[n1,m1] in [:(NatDivisors n),(NatDivisors m):]
by A53, ZFMISC_1:def 2;
set x =
((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1];
A58:
[n1,m1] in [:(NatDivisors n),(NatDivisors m):]
by A53, ZFMISC_1:def 2;
(f | (NatDivisors (n * m))) . y =
f . y
by A49, A51, A52, FUNCT_1:49
.=
(f . n19) * (f . m19)
by A1, A54, A55, 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:75
.=
multnat . ([:f,f:] . [n1,m1])
by BINOP_1:def 1
.=
(multnat * [:f,f:]) . [n1,m1]
by A21, FUNCT_1:13
.=
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1]
by A58, FUNCT_1:49
;
then
[n1,m1] in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
by A56, PRE_POLY:def 7;
then A59:
[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:33;
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:3;
then A60:
((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:33;
A61:
y =
multnat . (
n1,
m1)
by A54, BINOP_2:def 24
.=
multnat . [n1,m1]
by BINOP_1:def 1
.=
(multnat | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1]
by A57, FUNCT_1:49
.=
h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1]))
by A59, FUNCT_1:35
.=
(h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1])
by A60, FUNCT_1:13
;
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . (((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1]) = [n1,m1]
by A59, FUNCT_1:35;
then
((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1] in dom (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by A7, A57, A60, FUNCT_1:11;
hence
y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by A61, FUNCT_1:def 3;
verum
end;
then
rng (canFS (support (f | (NatDivisors (n * m))))) c= rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by TARSKI:def 3;
then
dom ((canFS (support (f | (NatDivisors (n * m))))) ") c= rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by FUNCT_1:33;
then
rng (((canFS (support (f | (NatDivisors (n * m))))) ") * (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) = rng ((canFS (support (f | (NatDivisors (n * m))))) ")
by RELAT_1:28;
then A62:
rng (((canFS (support (f | (NatDivisors (n * m))))) ") * (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))) = dom (canFS (support (f | (NatDivisors (n * m)))))
by FUNCT_1:33;
support (f | (NatDivisors (n * m))) c= dom (f | (NatDivisors (n * m)))
by PRE_POLY:37;
then
rng (canFS (support (f | (NatDivisors (n * m))))) c= dom (f | (NatDivisors (n * m)))
by FUNCT_2:def 3;
then
dom ((f | (NatDivisors (n * m))) * (canFS (support (f | (NatDivisors (n * m)))))) = dom (canFS (support (f | (NatDivisors (n * m)))))
by RELAT_1:27;
then A63:
rng ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f1
by A4, A62, RELAT_1:36;
then
for
x being
set holds
(
x in dom f2 iff (
x in dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) &
((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) . x in dom f1 ) )
by A32, FUNCT_1:3;
then
f2 = f1 * ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by A33, FUNCT_1:10;
then A64:
f1,
f2 are_fiberwise_equipotent
by A32, A63, CLASSES1:77;
thus F . (n * m) =
Sum (f | (NatDivisors (n * m)))
by A2
.=
Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
by A3, A5, A64, RFINSEQ:9
.=
(Sum (f | (NatDivisors n))) * (Sum (f | (NatDivisors m)))
by Th28
.=
(Sum (f | (NatDivisors n))) * (F . m)
by A2
.=
(F . n) * (F . m)
by A2
;
verum
end;
hence
F is multiplicative
by Def5; verum