let m be FinSequence of NAT ; :: thesis: ( len m >= 4 implies IDEAoperationC (IDEAoperationC m) = m )
assume A1: len m >= 4 ; :: thesis: IDEAoperationC (IDEAoperationC m) = m
consider I1 being FinSequence of NAT such that
A2: I1 = IDEAoperationC m ;
consider I2 being FinSequence of NAT such that
A3: I2 = IDEAoperationC I1 ;
A4: Seg (len m) = dom m by FINSEQ_1:def 3;
A5: Seg (len m) = Seg (len I1) by A2, Def13
.= Seg (len I2) by A3, Def13
.= dom I2 by FINSEQ_1:def 3 ;
3 <= len m by A1, XXREAL_0:2;
then 3 in Seg (len m) by FINSEQ_1:3;
then 3 in dom m by FINSEQ_1:def 3;
then A6: I1 . 3 = m . 2 by A2, Lm4;
2 <= len m by A1, XXREAL_0:2;
then 2 in Seg (len m) by FINSEQ_1:3;
then 2 in dom m by FINSEQ_1:def 3;
then A7: I1 . 2 = m . 3 by A2, Lm3;

now

let j be Nat; :: thesis: ( j in Seg (len m) implies I2 . j = m . j )
assume A8: j in Seg (len m) ; :: thesis: I2 . j = m . j
then j in Seg (len I1) by A2, Def13;
then A9: j in dom I1 by FINSEQ_1:def 3;
A10: j in dom m by A8, FINSEQ_1:def 3;

now

per cases ( j = 2 or j = 3 or ( j <> 2 & j <> 3 ) ) ;

suppose j = 2 ; :: thesis: I2 . j = m . j

hence I2 . j = m . j by A3, A6, A9, Lm3; :: thesis: verum

end;

suppose j = 3 ; :: thesis: I2 . j = m . j

hence I2 . j = m . j by A3, A7, A9, Lm4; :: thesis: verum

end;

suppose A11: ( j <> 2 & j <> 3 ) ; :: thesis: I2 . j = m . j

hence I2 . j = I1 . j by A3, A9, Lm5
.= m . j by A2, A10, A11, Lm5 ;
:: thesis: verum

end;

end;

end;

hence I2 . j = m . j ; :: thesis: verum

end;

hence IDEAoperationC (IDEAoperationC m) = m by A2, A3, A4, A5, FINSEQ_1:17; :: thesis: verum