let i, j be Element of NAT ; :: thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 - R2) . j = (R1 . j) - (R2 . j)
let R1, R2 be Element of i -tuples_on COMPLEX; :: thesis: (R1 - R2) . j = (R1 . j) - (R2 . j)

per cases ( not j in Seg i or j in Seg i ) ;

suppose A1: not j in Seg i ; :: thesis: (R1 - R2) . j = (R1 . j) - (R2 . j)

then A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1, FINSEQ_2:124;
not j in dom (R1 - R2) by A1, FINSEQ_2:124;
hence (R1 - R2) . j = 0 - 0 by FUNCT_1:def 2
.= (R1 . j) - 0 by A3, FUNCT_1:def 2
.= (R1 . j) - (R2 . j) by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

suppose j in Seg i ; :: thesis: (R1 - R2) . j = (R1 . j) - (R2 . j)

then j in dom (R1 - R2) by FINSEQ_2:124;
hence (R1 - R2) . j = (R1 . j) - (R2 . j) by VALUED_1:13; :: thesis: verum

end;

end;