let k be Nat; (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))
A1:
dom FIB = NAT
by FUNCT_2:def 1;
FIB | (OddNAT /\ (Seg ((2 * k) + 5))) =
FIB | ((OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)})
by Th62
.=
(FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ (FIB | {((2 * k) + 5)})
by RELAT_1:78
.=
(FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]}
by A1, GRFUNC_1:28
;
hence
(FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))
; verum