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