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