let X be non empty disjoint_with_NAT set ; :: thesis: EmptyIns (FreeUnivAlgNSG (ECIW-signature,X)) = 1 -tree {}
set S = ECIW-signature ;
reconsider s = ECIW-signature as non empty FinSequence of omega ;
set A = FreeUnivAlgNSG (ECIW-signature,X);
A1: 1 in dom the charact of (FreeUnivAlgNSG (ECIW-signature,X)) by Def10;
reconsider f = the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 1 as non empty homogeneous quasi_total nullary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) by Def10;
A2: f = FreeOpNSG (1,ECIW-signature,X) by A1, FREEALG:def 12;
A3: 1 in dom ECIW-signature by Th54;
then A4: s /. 1 = ECIW-signature . 1 by PARTFUN1:def 8;
A5: dom (FreeOpNSG (1,ECIW-signature,X)) = (s /. 1) -tuples_on (TS (DTConUA (ECIW-signature,X))) by A3, FREEALG:def 11
.= {{}} by A4, Th54, COMPUT_1:8 ;
A6: {} in {{}} by TARSKI:def 1;
A7: {} = <*> (TS (DTConUA (ECIW-signature,X))) ;
thus EmptyIns (FreeUnivAlgNSG (ECIW-signature,X)) = f . {} by A1, FUNCT_7:def 1
.= (Sym (1,ECIW-signature,X)) -tree {} by A2, A3, A5, A6, A7, FREEALG:def 11
.= 1 -tree {} by A3, FREEALG:def 10 ; :: thesis: verum