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 {{} } & {} = <*> (TS (DTConUA ECIW-signature ,X)) ) by TARSKI:def 1;
thus EmptyIns (FreeUnivAlgNSG ECIW-signature ,X) = f . {} by A1, FUNCT_7:def 1
.= (Sym 1,ECIW-signature ,X) -tree {} by A2, A5, A6, A3, FREEALG:def 11
.= 1 -tree {} by A3, FREEALG:def 10 ; :: thesis: verum