let X be non empty disjoint_with_NAT set ; :: thesis: for C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) holds while C,I = 4 -tree C,I
set S = ECIW-signature ;
reconsider s = ECIW-signature as non empty FinSequence of omega ;
set A = FreeUnivAlgNSG ECIW-signature ,X;
let C, I be Element of (FreeUnivAlgNSG ECIW-signature ,X); :: thesis: while C,I = 4 -tree C,I
A1: 4 in dom the charact of (FreeUnivAlgNSG ECIW-signature ,X) by Def13;
reconsider f = the charact of (FreeUnivAlgNSG ECIW-signature ,X) . 4 as non empty homogeneous quasi_total binary PartFunc of (the carrier of (FreeUnivAlgNSG ECIW-signature ,X) * ),the carrier of (FreeUnivAlgNSG ECIW-signature ,X) by Def13;
A2: f = FreeOpNSG 4,ECIW-signature ,X by A1, FREEALG:def 12;
A3: 4 in dom ECIW-signature by Th54;
then s /. 4 = ECIW-signature . 4 by PARTFUN1:def 8;
then A4: dom (FreeOpNSG 4,ECIW-signature ,X) = 2 -tuples_on (TS (DTConUA ECIW-signature ,X)) by A3, Th54, FREEALG:def 11;
A5: <*C,I*> in 2 -tuples_on (TS (DTConUA ECIW-signature ,X)) by FINSEQ_2:157;
thus while C,I = f . <*C,I*> by A1, FUNCT_7:def 1
.= (Sym 4,ECIW-signature ,X) -tree <*C,I*> by A2, A3, A4, A5, FREEALG:def 11
.= 4 -tree C,I by A3, FREEALG:def 10 ; :: thesis: verum