set f = rseq (a,b,0,0);
let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom (rseq (a,b,0,0)) or not y in dom (rseq (a,b,0,0)) or (rseq (a,b,0,0)) . x = (rseq (a,b,0,0)) . y )
assume ( x in dom (rseq (a,b,0,0)) & y in dom (rseq (a,b,0,0)) ) ; :: thesis: (rseq (a,b,0,0)) . x = (rseq (a,b,0,0)) . y
then reconsider n = x, m = y as Nat ;
thus (rseq (a,b,0,0)) . x = ((a * n) + b) / ((0 * n) + 0) by Th5
.= ((a * m) + b) / ((0 * m) + 0)
.= (rseq (a,b,0,0)) . y by Th5 ; :: thesis: verum