let n be Nat; for m being FinSequence of NAT st len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n holds
( (IDEAoperationC m) . 1 is_expressible_by n & (IDEAoperationC m) . 2 is_expressible_by n & (IDEAoperationC m) . 3 is_expressible_by n & (IDEAoperationC m) . 4 is_expressible_by n )
let m be FinSequence of NAT ; ( len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n implies ( (IDEAoperationC m) . 1 is_expressible_by n & (IDEAoperationC m) . 2 is_expressible_by n & (IDEAoperationC m) . 3 is_expressible_by n & (IDEAoperationC m) . 4 is_expressible_by n ) )
assume that
A1:
len m >= 4
and
A2:
( m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n )
; ( (IDEAoperationC m) . 1 is_expressible_by n & (IDEAoperationC m) . 2 is_expressible_by n & (IDEAoperationC m) . 3 is_expressible_by n & (IDEAoperationC m) . 4 is_expressible_by n )
1 <= len m
by A1, XXREAL_0:2;
then
1 in Seg (len m)
by FINSEQ_1:1;
then A3:
1 in dom m
by FINSEQ_1:def 3;
3 <= len m
by A1, XXREAL_0:2;
then
3 in Seg (len m)
by FINSEQ_1:1;
then A4:
3 in dom m
by FINSEQ_1:def 3;
2 <= len m
by A1, XXREAL_0:2;
then
2 in Seg (len m)
by FINSEQ_1:1;
then A5:
2 in dom m
by FINSEQ_1:def 3;
4 in Seg (len m)
by A1, FINSEQ_1:1;
then
4 in dom m
by FINSEQ_1:def 3;
hence
( (IDEAoperationC m) . 1 is_expressible_by n & (IDEAoperationC m) . 2 is_expressible_by n & (IDEAoperationC m) . 3 is_expressible_by n & (IDEAoperationC m) . 4 is_expressible_by n )
by A2, A3, A5, A4, Lm3, Lm4, Lm5; verum