let m be FinSequence of NAT ; :: thesis: for i being Nat st i = 2 & i in dom m holds

(IDEAoperationC m) . i = m . 3

let i be Nat; :: thesis: ( i = 2 & i in dom m implies (IDEAoperationC m) . i = m . 3 )

assume that

A1: i = 2 and

A2: i in dom m ; :: thesis: (IDEAoperationC m) . i = m . 3

(IDEAoperationC m) . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) by A2, Def13

.= m . 3 by A1, FUNCOP_1:def 8 ;

hence (IDEAoperationC m) . i = m . 3 ; :: thesis: verum

(IDEAoperationC m) . i = m . 3

let i be Nat; :: thesis: ( i = 2 & i in dom m implies (IDEAoperationC m) . i = m . 3 )

assume that

A1: i = 2 and

A2: i in dom m ; :: thesis: (IDEAoperationC m) . i = m . 3

(IDEAoperationC m) . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) by A2, Def13

.= m . 3 by A1, FUNCOP_1:def 8 ;

hence (IDEAoperationC m) . i = m . 3 ; :: thesis: verum