set f = rseq (0,b,0,d);
let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom (rseq (0,b,0,d)) or not y in dom (rseq (0,b,0,d)) or (rseq (0,b,0,d)) . x = (rseq (0,b,0,d)) . y )
assume that
A1: x in dom (rseq (0,b,0,d)) and
A2: y in dom (rseq (0,b,0,d)) ; :: thesis: (rseq (0,b,0,d)) . x = (rseq (0,b,0,d)) . y
thus (rseq (0,b,0,d)) . x = b / d by A1, Th6
.= (rseq (0,b,0,d)) . y by A2, Th6 ; :: thesis: verum