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 0 -ary 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 11;
A3: 1 in dom ECIW-signature by Th54;
then A4: s /. 1 = ECIW-signature . 1 by PARTFUN1:def 6;
A5: dom (FreeOpNSG (1,ECIW-signature,X)) = (s /. 1) -tuples_on (TS (DTConUA (ECIW-signature,X))) by A3, FREEALG:def 10
.= {{}} by A4, Th54, COMPUT_1:5 ;
A6: {} in {{}} by TARSKI:def 1;
A7: {} = <*> (TS (DTConUA (ECIW-signature,X))) ;
thus EmptyIns (FreeUnivAlgNSG (ECIW-signature,X)) = f . {} by A1, SUBSET_1:def 8
.= (Sym (1,ECIW-signature,X)) -tree {} by A2, A3, A5, A6, A7, FREEALG:def 10
.= 1 -tree {} by A3, FREEALG:def 9 ; :: thesis: verum