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 ;
:: according to REALSET1:def 6 :: thesis: ( not x in [:S,S:] or (multint n) . x in S )
assume
x in [:S,S:]
;
:: thesis: (multint n) . x in S
then consider a,
b being
set such that A2:
(
a in Segm0 n &
b in Segm0 n &
x = [a,b] )
by ZFMISC_1:def 2;
A3:
a in (Segm n) \ {0 }
by A1, A2, Def2;
then reconsider a1 =
a as
Element of
(INT.Ring n) by XBOOLE_0:def 5;
A4:
b in (Segm n) \ {0 }
by A1, A2, Def2;
then reconsider b1 =
b as
Element of
(INT.Ring n) by XBOOLE_0:def 5;
set y =
(multint n) . a,
b;
A5:
(multint n) . a,
b = a1 * b1
;
A6:
0 in Segm n
by GR_CY_1:10;
not
a in {0 }
by A3, XBOOLE_0:def 5;
then
a <> 0
by TARSKI:def 1;
then A7:
a <> 0. (INT.Ring n)
by A6, FUNCT_7:def 1;
not
b in {0 }
by A4, XBOOLE_0:def 5;
then
b <> 0
by TARSKI:def 1;
then A8:
b <> 0. (INT.Ring n)
by A6, FUNCT_7:def 1;
(multint n) . a,
b <> In 0 ,
(Segm n)
by A5, A7, A8, VECTSP_1:44;
then
(multint n) . a,
b <> 0
by A5, 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 A5, XBOOLE_0:def 5;
hence
(multint n) . x in S
by A1, A2, Def2;
:: thesis: verum
end;
hence
(multint n) || (Segm0 n) is BinOp of Segm0 n
by REALSET1:9; :: thesis: verum