let s be set ; :: thesis: for i being natural Number
for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)
let i be natural Number ; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)
let R1, R2 be Element of i -tuples_on REAL; :: thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)

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

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

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

end;

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

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

end;

end;