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 ; :: according to REALSET1:def 4 :: thesis: ( 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:] ; :: thesis: (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; :: thesis: verum

end;

hence (multint n) || (Segm0 n) is BinOp of (Segm0 n) by REALSET1:6; :: thesis: verum