A1:
1 < n
by INT_2:def 4;
then
Segm0 n = (Segm n) \ {0}
by Def2;
then reconsider S = Segm0 n as Subset of (Segm n) by XBOOLE_1:36;
multint n is S -subsetpreserving
proof
let x be
set ;
REALSET1:def 4 ( not x in [:S,S:] or (multint n) . x in S )
A2:
0 in Segm n
by NAT_1:44;
assume
x in [:S,S:]
;
(multint n) . x in S
then consider a,
b being
object such that A3:
a in Segm0 n
and A4:
b in Segm0 n
and A5:
x = [a,b]
by ZFMISC_1:def 2;
A6:
b in (Segm n) \ {0}
by A1, A4, Def2;
then reconsider b1 =
b as
Element of
(INT.Ring n) by XBOOLE_0:def 5;
not
b in {0}
by A6, XBOOLE_0:def 5;
then
b <> 0
by TARSKI:def 1;
then A7:
b <> 0. (INT.Ring n)
by A2, SUBSET_1:def 8;
A8:
a in (Segm n) \ {0}
by A1, A3, Def2;
then reconsider a1 =
a as
Element of
(INT.Ring n) by XBOOLE_0:def 5;
set y =
(multint n) . (
a,
b);
A9:
(multint n) . (
a,
b)
= a1 * b1
;
not
a in {0}
by A8, XBOOLE_0:def 5;
then
a <> 0
by TARSKI:def 1;
then
a <> 0. (INT.Ring n)
by A2, SUBSET_1:def 8;
then
(multint n) . (
a,
b)
<> In (
0,
(Segm n))
by A9, A7, VECTSP_1:12;
then
(multint n) . (
a,
b)
<> 0
by A9;
then
not
(multint n) . (
a,
b)
in {0}
by TARSKI:def 1;
then
(multint n) . (
a,
b)
in (Segm n) \ {0}
by A9, XBOOLE_0:def 5;
hence
(multint n) . x in S
by A1, A5, Def2;
verum
end;
hence
(multint n) || (Segm0 n) is BinOp of (Segm0 n)
by REALSET1:6; verum