let f, F be sequence of NAT; :: thesis: ( 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 ; :: thesis: ( 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)) ; :: thesis: F is multiplicative

for n, m being non zero Nat st n,m are_coprime holds

F . (n * m) = (F . n) * (F . m)

assume A1: f is multiplicative ; :: thesis: ( 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)) ; :: thesis: F is multiplicative

for n, m being non zero Nat st n,m are_coprime holds

F . (n * m) = (F . n) * (F . m)

proof

hence
F is multiplicative
; :: thesis: verum
let n, m be non zero Nat; :: thesis: ( 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 ; :: thesis: 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

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)

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)

y in 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 ; :: thesis: verum

end;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 ; :: thesis: 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

then reconsider h9 = multnat | [:(NatDivisors n),(NatDivisors m):] as one-to-one Function by FUNCT_1:def 4;
let x1, x2 be object ; :: 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 A9: 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 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):]) ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;assume A9: 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 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):]) ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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

then
support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]) c= dom (((canFS (support (f | (NatDivisors (n * m))))) ") * h9)
;
let x be object ; :: thesis: ( 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):]) ; :: thesis: 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; :: thesis: verum

end;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):]) ; :: thesis: 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; :: thesis: verum

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

for y being object st y in rng (canFS (support (f | (NatDivisors (n * m))))) holds
let x be object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: verum

y in rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))

proof

then
rng (canFS (support (f | (NatDivisors (n * m))))) c= rng (h9 * (canFS (support ((multnat * [:f,f:]) | [:(NatDivisors n),(NatDivisors m):]))))
;
let y be object ; :: thesis: ( 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))))) ; :: thesis: 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; :: thesis: verum

end;assume y in rng (canFS (support (f | (NatDivisors (n * m))))) ; :: thesis: 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; :: thesis: verum

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 ; :: thesis: verum