A1:
1 < n
by INT_2:def 5;
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 Presv of Segm n,S
proof
let x be
set ;
REALSET1:def 6 ( not x in [:S,S:] or (multint n) . x in S )
A2:
0 in Segm n
by NAT_1:45;
assume
x in [:S,S:]
;
(multint n) . x in S
then consider a,
b being
set 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, FUNCT_7:def 1;
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, FUNCT_7:def 1;
then
(multint n) . a,
b <> In 0 ,
(Segm n)
by A9, A7, VECTSP_1:44;
then
(multint n) . a,
b <> 0
by A9, FUNCT_7:def 1;
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:9; verum