A2:
f |^ 0 = 1_ A
by BINOM:8;
A4:
1. A in multClSet (J,f)
by A2;
for v, u being Element of A st v in multClSet (J,f) & u in multClSet (J,f) holds
v * u in multClSet (J,f)
proof
let v,
u be
Element of
A;
( v in multClSet (J,f) & u in multClSet (J,f) implies v * u in multClSet (J,f) )
assume that A5:
v in multClSet (
J,
f)
and A6:
u in multClSet (
J,
f)
;
v * u in multClSet (J,f)
consider n1 being
Nat such that A7:
v = f |^ n1
by A5;
consider n2 being
Nat such that A8:
u = f |^ n2
by A6;
v * u = f |^ (n1 + n2)
by BINOM:10, A8, A7;
hence
v * u in multClSet (
J,
f)
;
verum
end;
hence
multClSet (J,f) is multiplicatively-closed
by A4, C0SP1:def 4; verum