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

A6: now :: thesis: for j being Nat st j in Seg (len m) holds
I2 . j = m . j

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

now :: thesis: I2 . j = m . j

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 A4, A5, A8, Lm3; :: thesis: verum

end;

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

hence I2 . j = m . j by A4, A3, A8, Lm4; :: thesis: verum

end;

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

hence I2 . j = I1 . j by A4, A8, Lm5
.= m . j by A1, A9, A10, Lm5 ;
:: thesis: verum

end;

end;

end;

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

end;

A11: Seg (len m) = dom m by FINSEQ_1:def 3;
Seg (len m) = Seg (len I1) by A1, Def13
.= Seg (len I2) by A4, Def13
.= dom I2 by FINSEQ_1:def 3 ;
hence IDEAoperationC (IDEAoperationC m) = m by A1, A4, A11, A6, FINSEQ_1:13; :: thesis: verum