let f be non empty FinSequence of NAT ; :: thesis: for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f
let D be non empty disjoint_with_NAT set ; :: thesis: signature (FreeUnivAlgNSG (f,D)) = f
set fa = FreeUnivAlgNSG (f,D);
set A = TS (DTConUA (f,D));
A1: len the charact of (FreeUnivAlgNSG (f,D)) = len f by Def11;
A2: len (signature (FreeUnivAlgNSG (f,D))) = len the charact of (FreeUnivAlgNSG (f,D)) by UNIALG_1:def 4;
then A3: dom (signature (FreeUnivAlgNSG (f,D))) = Seg (len f) by A1, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom (signature (FreeUnivAlgNSG (f,D))) holds
(signature (FreeUnivAlgNSG (f,D))) . n = f . n

let n be Nat; :: thesis: ( n in dom (signature (FreeUnivAlgNSG (f,D))) implies (signature (FreeUnivAlgNSG (f,D))) . n = f . n )
reconsider h = FreeOpNSG (n,f,D) as non empty homogeneous quasi_total PartFunc of ( the carrier of (FreeUnivAlgNSG (f,D)) *), the carrier of (FreeUnivAlgNSG (f,D)) ;
A4: dom h = (arity h) -tuples_on the carrier of (FreeUnivAlgNSG (f,D)) by MARGREL1:22;
assume A5: n in dom (signature (FreeUnivAlgNSG (f,D))) ; :: thesis: (signature (FreeUnivAlgNSG (f,D))) . n = f . n
then A6: n in dom f by A3, FINSEQ_1:def 3;
then dom h = (f /. n) -tuples_on (TS (DTConUA (f,D))) by Def10;
then A7: arity h = f /. n by A4, FINSEQ_2:110;
n in dom (FreeOpSeqNSG (f,D)) by A1, A3, A5, FINSEQ_1:def 3;
then the charact of (FreeUnivAlgNSG (f,D)) . n = FreeOpNSG (n,f,D) by Def11;
hence (signature (FreeUnivAlgNSG (f,D))) . n = arity h by A5, UNIALG_1:def 4
.= f . n by A6, A7, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence signature (FreeUnivAlgNSG (f,D)) = f by A2, A1, FINSEQ_2:9; :: thesis: verum