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:def 1; :: thesis: verum
end;
end;