let i, n, j be Nat; :: thesis: ( 1 <= i & i <= n & i <> j implies |((Base_FinSeq n,i),(Base_FinSeq n,j))| = 0 )
assume that
A1: 1 <= i and
A2: i <= n and
A3: i <> j ; :: thesis: |((Base_FinSeq n,i),(Base_FinSeq n,j))| = 0
set x1 = Base_FinSeq n,i;
set x2 = Base_FinSeq n,j;
A4: dom (0* n) = Seg (len (n |-> 0 )) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
A5: dom (Base_FinSeq n,j) = Seg (len (Base_FinSeq n,j)) by FINSEQ_1:def 3
.= Seg n by MATRIXR2:74 ;
A6: dom (Base_FinSeq n,i) = Seg (len (Base_FinSeq n,i)) by FINSEQ_1:def 3
.= Seg n by MATRIXR2:74 ;
A7: dom <:(Base_FinSeq n,i),(Base_FinSeq n,j):> = (dom (Base_FinSeq n,i)) /\ (dom (Base_FinSeq n,j)) by FUNCT_3:def 8;
dom multreal = [:REAL ,REAL :] by FUNCT_2:def 1;
then A8: dom (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) = <:(Base_FinSeq n,i),(Base_FinSeq n,j):> " [:REAL ,REAL :] by RELAT_1:182
.= Seg n by A7, A6, A5, RELSET_1:38 ;
for x being set st x in dom (0* n) holds
(multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x

proof

let x be set ; :: thesis: ( x in dom (0* n) implies (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x )
assume A9: x in dom (0* n) ; :: thesis: (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x
then reconsider nx = x as Element of NAT ;
A10: (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = multreal . (<:(Base_FinSeq n,i),(Base_FinSeq n,j):> . x) by A4, A8, A9, FUNCT_1:22
.= multreal . [((Base_FinSeq n,i) . nx),((Base_FinSeq n,j) . nx)] by A4, A7, A6, A5, A9, FUNCT_3:def 8 ;
A11: nx <= n by A4, A9, FINSEQ_1:3;
A12: 1 <= nx by A4, A9, FINSEQ_1:3;

per cases ( nx = i or nx <> i ) ;

suppose A13: nx = i ; :: thesis: (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x

then A14: (Base_FinSeq n,i) . nx = 1 by A1, A2, MATRIXR2:75;
A15: (Base_FinSeq n,j) . nx = 0 by A1, A2, A3, A13, MATRIXR2:76;
multreal . [((Base_FinSeq n,i) . nx),((Base_FinSeq n,j) . nx)] = multreal . ((Base_FinSeq n,i) . nx),((Base_FinSeq n,j) . nx)
.= 1 * 0 by A15, A14, BINOP_2:def 11
.= 0 ;
hence (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x by A4, A9, A10, FINSEQ_2:71; :: thesis: verum

end;

suppose A16: nx <> i ; :: thesis: (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x

reconsider r = (Base_FinSeq n,j) . nx as Element of REAL ;
A17: (Base_FinSeq n,i) . nx = 0 by A12, A11, A16, MATRIXR2:76;
multreal . [((Base_FinSeq n,i) . nx),((Base_FinSeq n,j) . nx)] = multreal . ((Base_FinSeq n,i) . nx),((Base_FinSeq n,j) . nx)
.= 0 * r by A17, BINOP_2:def 11
.= 0 ;
hence (multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):>) . x = (0* n) . x by A4, A9, A10, FINSEQ_2:71; :: thesis: verum

end;

end;

end;

then multreal * <:(Base_FinSeq n,i),(Base_FinSeq n,j):> = 0* n by A4, A8, FUNCT_1:9;
then multreal .: (Base_FinSeq n,i),(Base_FinSeq n,j) = 0* n by FUNCOP_1:def 3;
hence |((Base_FinSeq n,i),(Base_FinSeq n,j))| = 0 by RVSUM_1:111; :: thesis: verum