let i, j, n 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 CARD_1:def 7 ;
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 7;
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:147
.= Seg n by A7, A6, A5, RELSET_1:22 ;
for x being object st x in dom (0* n) holds
(multreal * <:(Base_FinSeq (n,i)),(Base_FinSeq (n,j)):>) . x = (0* n) . x

proof

let x be object ; :: 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:12
.= multreal . [((Base_FinSeq (n,i)) . nx),((Base_FinSeq (n,j)) . nx)] by A4, A7, A6, A5, A9, FUNCT_3:def 7 ;
A11: nx <= n by A4, A9, FINSEQ_1:1;
A12: 1 <= nx by A4, A9, FINSEQ_1:1;

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 A10; :: 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 by XREAL_0:def 1;
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 A10; :: thesis: verum

end;

end;

end;

then multreal * <:(Base_FinSeq (n,i)),(Base_FinSeq (n,j)):> = 0* n by A4, A8, FUNCT_1:2;
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:81; :: thesis: verum