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 2 -ary 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 11;
A3: 4 in dom ECIW-signature by Th54;
then s /. 4 = ECIW-signature . 4 by PARTFUN1:def 6;
then A4: dom (FreeOpNSG (4,ECIW-signature,X)) = 2 -tuples_on (TS (DTConUA (ECIW-signature,X))) by A3, Th54, FREEALG:def 10;
A5: <*C,I*> in 2 -tuples_on (TS (DTConUA (ECIW-signature,X))) by FINSEQ_2:137;
thus while (C,I) = f . <*C,I*> by A1, SUBSET_1:def 8
.= (Sym (4,ECIW-signature,X)) -tree <*C,I*> by A2, A3, A4, A5, FREEALG:def 10
.= 4 -tree (C,I) by A3, FREEALG:def 9 ; :: thesis: verum