let f, F be sequence of NAT; ( f is multiplicative & ( for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ) implies F is multiplicative )
assume A1:
f is multiplicative
; ( ex n0 being non zero Nat st not F . n0 = Sum (f | (NatDivisors n0)) or F is multiplicative )
assume A2:
for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0))
; F is multiplicative
for n, m being non zero Nat st n,m are_coprime holds
F . (n * m) = (F . n) * (F . m)
proof
let n,
m be non
zero Nat;
( n,m are_coprime 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_coprime
;
F . (n * m) = (F . n) * (F . m)
for
x1,
x2 being
object 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
object ;
( 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
object such that A10:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A11:
x1 = [n1,m1]
by 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
object such that A14:
n2 in NatDivisors n
and A15:
m2 in NatDivisors m
and A16:
x2 = [n2,m2]
by 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;
A20:
dom [:f,f:] = [:NAT,NAT:]
by FUNCT_2:def 1;
for
x being
object 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
object ;
( x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) implies x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9) )
A21:
rng (canFS (support (f | (NatDivisors (n * m))))) = support (f | (NatDivisors (n * m)))
by FUNCT_2:def 3;
assume A22:
x in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
;
x in dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
then A23:
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . x <> 0
by PRE_POLY:def 7;
A24:
x in [:(NatDivisors n),(NatDivisors m):]
by A22;
consider n1,
m1 being
object such that A25:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A26:
x = [n1,m1]
by A22, ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by A25;
A27:
n1,
m1 are_coprime
by A8, A25, Th14;
reconsider n19 =
n1,
m19 =
m1 as non
zero Nat by A25;
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 A22, FUNCT_1:49
.=
multnat . ([:f,f:] . x)
by A20, A24, FUNCT_1:13
.=
multnat . ([:f,f:] . (n1,m1))
by A26, 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, A27
.=
(f | (NatDivisors (n * m))) . (n1 * m1)
by A25, Th16, FUNCT_1:49
;
then A28:
n1 * m1 in rng (canFS (support (f | (NatDivisors (n * m)))))
by A23, A21, 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 A29:
((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 A28, FUNCT_1:35
.=
multnat . (
n1,
m1)
by BINOP_2:def 24
.=
multnat . [n1,m1]
by BINOP_1:def 1
.=
h9 . x
by A22, A26, FUNCT_1:49
;
then
h9 . x in rng (canFS (support (f | (NatDivisors (n * m)))))
by A29, 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, A22, FUNCT_1:11;
verum
end;
then
support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
;
then
rng (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
;
then A30:
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;
then A31:
dom ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f2
by A6, A30, RELAT_1:27;
A32:
for
x being
object 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
object ;
( 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;
A33:
((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 A34:
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 A35:
x in dom (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))
by A6, FUNCT_1:11;
then A36:
(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 A37:
(
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
object such that A38:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A39:
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x = [n1,m1]
by ZFMISC_1:def 2;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by A38;
A40:
n1,
m1 are_coprime
by A8, A38, Th14;
reconsider n19 =
n1,
m19 =
m1 as non
zero Nat by A38;
set fn1 =
f . n1;
set fm1 =
f . m1;
A41:
(canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x in [:(NatDivisors n),(NatDivisors m):]
by A37;
A42:
((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 A37, FUNCT_1:49
.=
multnat . ([:f,f:] . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x))
by A20, A41, FUNCT_1:13
.=
multnat . ([:f,f:] . (n1,m1))
by A39, 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, A40
;
A43:
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) <> 0
by A36, PRE_POLY:def 7;
f . (n19 * m19) = (f | (NatDivisors (n * m))) . (n1 * m1)
by A38, Th16, FUNCT_1:49;
then A44:
n1 * m1 in support (f | (NatDivisors (n * m)))
by A43, A42, PRE_POLY:def 7;
then A45:
n1 * m1 in dom (id (support (f | (NatDivisors (n * m)))))
;
A46:
h9 . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x) =
multnat . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)
by A7, A37, FUNCT_1:47
.=
multnat . (
n1,
m1)
by A39, BINOP_1:def 1
.=
n1 * m1
by BINOP_2:def 24
;
A47:
((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 A31, A34, 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 A35, 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, A37, FUNCT_1:13
.=
(f | (NatDivisors (n * m))) . ((id (support (f | (NatDivisors (n * m))))) . (n1 * m1))
by A45, A46, FUNCT_1:13
.=
(f | (NatDivisors (n * m))) . (n1 * m1)
by A44, FUNCT_1:18
.=
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . ((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) . x)
by A38, A42, 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, A35, A47, A33, FUNCT_1:13;
verum
end;
for
y being
object 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
object ;
( y in rng (canFS (support (f | (NatDivisors (n * m))))) implies y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) )
assume
y in rng (canFS (support (f | (NatDivisors (n * m)))))
;
y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
then A48:
y in support (f | (NatDivisors (n * m)))
by FUNCT_2:def 3;
consider n1,
m1 being
Nat such that A49:
(
n1 in NatDivisors n &
m1 in NatDivisors m )
and A50:
y = n1 * m1
by A8, A48, Th18;
reconsider n19 =
n1,
m19 =
m1 as non
zero Nat by A49;
reconsider n1 =
n1,
m1 =
m1 as
Element of
NAT by ORDINAL1:def 12;
A51:
n1,
m1 are_coprime
by A8, A49, Th14;
A52:
(f | (NatDivisors (n * m))) . y <> 0
by A48, PRE_POLY:def 7;
A53:
[n1,m1] in [:(NatDivisors n),(NatDivisors m):]
by A49, ZFMISC_1:def 2;
set x =
((canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))) ") . [n1,m1];
A54:
[n1,m1] in [:(NatDivisors n),(NatDivisors m):]
by A49, ZFMISC_1:def 2;
(f | (NatDivisors (n * m))) . y =
f . y
by A48, FUNCT_1:49
.=
(f . n19) * (f . m19)
by A1, A50, A51
.=
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 A20, FUNCT_1:13
.=
((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1]
by A54, FUNCT_1:49
;
then
[n1,m1] in support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
by A52, PRE_POLY:def 7;
then A55:
[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 A56:
((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;
A57:
y =
multnat . (
n1,
m1)
by A50, BINOP_2:def 24
.=
multnat . [n1,m1]
by BINOP_1:def 1
.=
(multnat | [:(NatDivisors n),(NatDivisors m):]) . [n1,m1]
by A53, 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 A55, 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 A56, 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 A55, 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, A53, A56, FUNCT_1:11;
hence
y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by A57, 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):]))))
;
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 A58:
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 A59:
rng ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])))) = dom f1
by A4, A58, RELAT_1:36;
then
for
x being
object 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 A31, FUNCT_1:3;
then
f2 = f1 * ((((canFS (support (f | (NatDivisors (n * m))))) ") * h9) * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
by A32, FUNCT_1:10;
then A60:
f1,
f2 are_fiberwise_equipotent
by A31, A59, CLASSES1:77;
thus F . (n * m) =
Sum (f | (NatDivisors (n * m)))
by A2
.=
Sum ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):])
by A3, A5, A60, 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
; verum