set S = FreeUnivAlgNSG (ECIW-signature,X);
set char = ECIW-signature ;
A1:
len <*0,2*> = 2
by FINSEQ_1:44;
A2:
len <*3,2*> = 2
by FINSEQ_1:44;
then A3:
len ECIW-signature = 2 + 2
by A1, FINSEQ_1:22;
A4:
len the charact of (FreeUnivAlgNSG (ECIW-signature,X)) = len ECIW-signature
by FREEALG:def 11;
A5:
dom <*0,2*> = Seg 2
by A1, FINSEQ_1:def 3;
A6:
dom <*3,2*> = Seg 2
by A2, FINSEQ_1:def 3;
A7:
dom the charact of (FreeUnivAlgNSG (ECIW-signature,X)) = Seg 4
by A3, A4, FINSEQ_1:def 3;
A8:
dom ECIW-signature = Seg 4
by A3, FINSEQ_1:def 3;
thus
1 in dom the charact of (FreeUnivAlgNSG (ECIW-signature,X))
by A7; AOFA_000:def 10 ( the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) & FreeUnivAlgNSG (ECIW-signature,X) is with_catenation & FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )
then A9:
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 1 = FreeOpNSG (1,ECIW-signature,X)
by FREEALG:def 11;
A10:
1 in dom ECIW-signature
by A8;
A11:
2 in dom ECIW-signature
by A8;
A12:
3 in dom ECIW-signature
by A8;
A13:
4 in dom ECIW-signature
by A8;
reconsider D = TS (DTConUA (ECIW-signature,X)) as non empty set ;
reconsider char = ECIW-signature as non empty FinSequence of omega ;
set o = FreeOpNSG (1,char,X);
A14:
1 in dom <*0,2*>
by A5;
A15:
<*0,2*> . 1 = 0
;
A16:
2 in dom <*0,2*>
by A5;
A17:
<*0,2*> . 2 = 2
;
char . 1 = 0
by A14, A15, FINSEQ_1:def 7;
then
char /. 1 = 0
by A10, PARTFUN1:def 6;
then A18:
dom (FreeOpNSG (1,char,X)) = 0 -tuples_on the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A10, FREEALG:def 10;
reconsider o = FreeOpNSG (1,char,X) as non empty homogeneous quasi_total PartFunc of (D *),D ;
arity o = 0
by A18, COMPUT_1:25;
hence
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A9, COMPUT_1:def 21; ( FreeUnivAlgNSG (ECIW-signature,X) is with_catenation & FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )
thus
2 in dom the charact of (FreeUnivAlgNSG (ECIW-signature,X))
by A7; AOFA_000:def 11 ( the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) & FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )
then A19:
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 2 = FreeOpNSG (2,char,X)
by FREEALG:def 11;
set o = FreeOpNSG (2,char,X);
char . 2 = 2
by A16, A17, FINSEQ_1:def 7;
then
char /. 2 = 2
by A11, PARTFUN1:def 6;
then A20:
dom (FreeOpNSG (2,char,X)) = 2 -tuples_on the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A11, FREEALG:def 10;
reconsider o = FreeOpNSG (2,char,X) as non empty homogeneous quasi_total PartFunc of (D *),D ;
arity o = 2
by A20, COMPUT_1:25;
hence
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A19, COMPUT_1:def 21; ( FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )
thus
3 in dom the charact of (FreeUnivAlgNSG (ECIW-signature,X))
by A7; AOFA_000:def 12 ( the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )
then A21:
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 3 = FreeOpNSG (3,char,X)
by FREEALG:def 11;
set o = FreeOpNSG (3,char,X);
A22:
1 in dom <*3,2*>
by A6;
A23:
<*3,2*> . 1 = 3
;
A24:
2 in dom <*3,2*>
by A6;
A25:
<*3,2*> . 2 = 2
;
char . (2 + 1) = 3
by A1, A22, A23, FINSEQ_1:def 7;
then
char /. 3 = 3
by A12, PARTFUN1:def 6;
then A26:
dom (FreeOpNSG (3,char,X)) = 3 -tuples_on the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A12, FREEALG:def 10;
reconsider o = FreeOpNSG (3,char,X) as non empty homogeneous quasi_total PartFunc of (D *),D ;
arity o = 3
by A26, COMPUT_1:25;
hence
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A21, COMPUT_1:def 21; FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction
thus
4 in dom the charact of (FreeUnivAlgNSG (ECIW-signature,X))
by A7; AOFA_000:def 13 the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
then A27:
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 4 = FreeOpNSG (4,char,X)
by FREEALG:def 11;
set o = FreeOpNSG (4,char,X);
char . (2 + 2) = 2
by A1, A24, A25, FINSEQ_1:def 7;
then
char /. 4 = 2
by A13, PARTFUN1:def 6;
then A28:
dom (FreeOpNSG (4,char,X)) = 2 -tuples_on the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A13, FREEALG:def 10;
reconsider o = FreeOpNSG (4,char,X) as non empty homogeneous quasi_total PartFunc of (D *),D ;
arity o = 2
by A28, COMPUT_1:25;
hence
the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X))
by A27, COMPUT_1:def 21; verum