set S = FreeUnivAlgNSG ECIW-signature ,X;
set char = ECIW-signature ;
A1: ( len <*0 ,2*> = 2 & len <*3,2*> = 2 ) by FINSEQ_1:61;
then A2: ( len ECIW-signature = 2 + 2 & len the charact of (FreeUnivAlgNSG ECIW-signature ,X) = len ECIW-signature & dom <*0 ,2*> = Seg 2 & dom <*3,2*> = Seg 2 ) by FINSEQ_1:35, FINSEQ_1:def 3, FREEALG:def 12;
then A3: ( dom the charact of (FreeUnivAlgNSG ECIW-signature ,X) = Seg 4 & dom ECIW-signature = Seg 4 ) by FINSEQ_1:def 3;
hence 1 in dom the charact of (FreeUnivAlgNSG ECIW-signature ,X) ; :: according to AOFA_000:def 10 :: thesis: ( 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 A4: the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 1 = FreeOpNSG 1,ECIW-signature ,X by FREEALG:def 12;
A5: ( 1 in dom ECIW-signature & 2 in dom ECIW-signature & 3 in dom ECIW-signature & 4 in dom ECIW-signature ) by A3;
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;
A6: ( 1 in dom <*0 ,2*> & <*0 ,2*> . 1 = 0 & 2 in dom <*0 ,2*> & <*0 ,2*> . 2 = 2 ) by A2, FINSEQ_1:61;
then char . 1 = 0 by FINSEQ_1:def 7;
then ( char /. 1 = 0 & the carrier of (FreeUnivAlgNSG ECIW-signature ,X) = D ) by A5, PARTFUN1:def 8;
then A7: dom (FreeOpNSG 1,char,X) = 0 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X) by A5, FREEALG:def 11;
reconsider o = FreeOpNSG 1,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 0 by A7, 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 A4, COMPUT_1:def 24; :: thesis: ( 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 A3; :: according to AOFA_000:def 11 :: thesis: ( 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 A8: 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 A6, FINSEQ_1:def 7;
then char /. 2 = 2 by A5, PARTFUN1:def 8;
then A9: dom (FreeOpNSG 2,char,X) = 2 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X) by A5, FREEALG:def 11;
reconsider o = FreeOpNSG 2,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 2 by A9, 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 A8, COMPUT_1:def 26; :: thesis: ( 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 A3; :: according to AOFA_000:def 12 :: thesis: ( 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 A10: the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 3 = FreeOpNSG 3,char,X by FREEALG:def 12;
set o = FreeOpNSG 3,char,X;
A11: ( 1 in dom <*3,2*> & <*3,2*> . 1 = 3 & 2 in dom <*3,2*> & <*3,2*> . 2 = 2 ) by A2, FINSEQ_1:61;
then char . (2 + 1) = 3 by A1, FINSEQ_1:def 7;
then char /. 3 = 3 by A5, PARTFUN1:def 8;
then A12: dom (FreeOpNSG 3,char,X) = 3 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X) by A5, FREEALG:def 11;
reconsider o = FreeOpNSG 3,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 3 by A12, 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 A10, COMPUT_1:def 27; :: thesis: FreeUnivAlgNSG ECIW-signature ,X is with_while-instruction
thus 4 in dom the charact of (FreeUnivAlgNSG ECIW-signature ,X) by A3; :: according to AOFA_000:def 13 :: thesis: 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 A13: 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, A11, FINSEQ_1:def 7;
then char /. 4 = 2 by A5, PARTFUN1:def 8;
then A14: dom (FreeOpNSG 4,char,X) = 2 -tuples_on the carrier of (FreeUnivAlgNSG ECIW-signature ,X) by A5, FREEALG:def 11;
reconsider o = FreeOpNSG 4,char,X as non empty homogeneous quasi_total PartFunc of (D * ),D ;
arity o = 2 by A14, 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 A13, COMPUT_1:def 26; :: thesis: verum