let m be FinSequence of NAT ; for i being Nat st i = 3 & i in dom m holds
(IDEAoperationC m) . i = m . 2
let i be Nat; ( i = 3 & i in dom m implies (IDEAoperationC m) . i = m . 2 )
assume that
A1:
i = 3
and
A2:
i in dom m
; (IDEAoperationC m) . i = m . 2
(IDEAoperationC m) . i =
IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i))))
by A2, Def13
.=
IFEQ (i,3,(m . 2),(m . i))
by A1, FUNCOP_1:def 8
.=
m . 2
by A1, FUNCOP_1:def 8
;
hence
(IDEAoperationC m) . i = m . 2
; verum