let m be FinSequence of NAT ; :: thesis: for i being Element of NAT st i = 3 & i in dom m holds
(IDEAoperationC m) . i = m . 2
let i be Element of NAT ; :: thesis: ( i = 3 & i in dom m implies (IDEAoperationC m) . i = m . 2 )
assume A1: ( i = 3 & i in dom m ) ; :: thesis: (IDEAoperationC m) . i = m . 2
then (IDEAoperationC m) . i = IFEQ i,2,(m . 3),(IFEQ i,3,(m . 2),(m . i)) by 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 ; :: thesis: verum