set f = rseq (0,b,0,d);
let x, y be object ; FUNCT_1:def 10 ( 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))
; (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
; verum