A1:
len <*0,2*> = 2
by FINSEQ_1:44;
A2:
len <*3,2*> = 2
by FINSEQ_1:44;
A3:
dom <*0,2*> = Seg 2
by A1, FINSEQ_1:def 3;
A4:
dom <*3,2*> = Seg 2
by A2, FINSEQ_1:def 3;
then A5:
1 in dom <*3,2*>
;
A6:
<*3,2*> . 1 = 3
by FINSEQ_1:44;
A7:
2 in dom <*3,2*>
by A4;
A8:
<*3,2*> . 2 = 2
by FINSEQ_1:44;
A9:
2 + 1 = 3
;
A10:
1 in dom <*0,2*>
by A3;
A11:
<*0,2*> . 1 = 0
by FINSEQ_1:44;
A12:
2 in dom <*0,2*>
by A3;
<*0,2*> . 2 = 2
by FINSEQ_1:44;
hence
( len ECIW-signature = 4 & dom ECIW-signature = Seg 4 & ECIW-signature . 1 = 0 & ECIW-signature . 2 = 2 & ECIW-signature . 3 = 3 & ECIW-signature . 4 = 2 )
by A1, A2, A5, A6, A7, A8, A9, A10, A11, A12, FINSEQ_1:22, FINSEQ_1:def 7; verum