set S = FreeUnivAlgNSG ECIW-signature ,X;
set char = ECIW-signature ;
A1:
len <*0 ,2*> = 2
by FINSEQ_1:61;
A2:
len <*3,2*> = 2
by FINSEQ_1:61;
then A3:
len ECIW-signature = 2 + 2
by A1, FINSEQ_1:35;
A4:
len the charact of (FreeUnivAlgNSG ECIW-signature ,X) = len ECIW-signature
by FREEALG:def 12;
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 nullary 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 12;
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
by FINSEQ_1:61;
A16:
2 in dom <*0 ,2*>
by A5;
A17:
<*0 ,2*> . 2 = 2
by FINSEQ_1:61;
char . 1 = 0
by A14, A15, FINSEQ_1:def 7;
then
char /. 1 = 0
by A10, PARTFUN1:def 8;
then A18:
dom (FreeOpNSG 1,char,X) = 0 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A10, FREEALG:def 11;
reconsider o = FreeOpNSG 1,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 0
by A18, COMPUT_1:28;
hence
the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 1 is non empty homogeneous quasi_total nullary PartFunc of (the carrier of (FreeUnivAlgNSG ECIW-signature ,X) * ),the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A9, COMPUT_1:def 24; ( 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 binary 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 12;
set o = FreeOpNSG 2,char,X;
char . 2 = 2
by A16, A17, FINSEQ_1:def 7;
then
char /. 2 = 2
by A11, PARTFUN1:def 8;
then A20:
dom (FreeOpNSG 2,char,X) = 2 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A11, FREEALG:def 11;
reconsider o = FreeOpNSG 2,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 2
by A20, COMPUT_1:28;
hence
the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 2 is non empty homogeneous quasi_total binary PartFunc of (the carrier of (FreeUnivAlgNSG ECIW-signature ,X) * ),the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A19, COMPUT_1:def 26; ( 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 ternary 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 12;
set o = FreeOpNSG 3,char,X;
A22:
1 in dom <*3,2*>
by A6;
A23:
<*3,2*> . 1 = 3
by FINSEQ_1:61;
A24:
2 in dom <*3,2*>
by A6;
A25:
<*3,2*> . 2 = 2
by FINSEQ_1:61;
char . (2 + 1) = 3
by A1, A22, A23, FINSEQ_1:def 7;
then
char /. 3 = 3
by A12, PARTFUN1:def 8;
then A26:
dom (FreeOpNSG 3,char,X) = 3 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A12, FREEALG:def 11;
reconsider o = FreeOpNSG 3,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 3
by A26, COMPUT_1:28;
hence
the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 3 is non empty homogeneous quasi_total ternary PartFunc of (the carrier of (FreeUnivAlgNSG ECIW-signature ,X) * ),the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A21, COMPUT_1:def 27; 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 binary 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 12;
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 8;
then A28:
dom (FreeOpNSG 4,char,X) = 2 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A13, FREEALG:def 11;
reconsider o = FreeOpNSG 4,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 2
by A28, COMPUT_1:28;
hence
the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 4 is non empty homogeneous quasi_total binary PartFunc of (the carrier of (FreeUnivAlgNSG ECIW-signature ,X) * ),the carrier of (FreeUnivAlgNSG ECIW-signature ,X)
by A27, COMPUT_1:def 26; verum