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

now

let n be Nat; :: thesis: ( n in dom (signature (FreeUnivAlgZAO f,D)) implies (signature (FreeUnivAlgZAO f,D)) . n = f . n )
reconsider h = FreeOpZAO n,f,D as non empty homogeneous quasi_total PartFunc of (the carrier of (FreeUnivAlgZAO f,D) * ),the carrier of (FreeUnivAlgZAO f,D) ;
A4: dom h = (arity h) -tuples_on the carrier of (FreeUnivAlgZAO f,D) by UNIALG_2:2;
assume A5: n in dom (signature (FreeUnivAlgZAO f,D)) ; :: thesis: (signature (FreeUnivAlgZAO 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 Def17;
then A7: arity h = f /. n by A4, FINSEQ_2:130;
n in dom (FreeOpSeqZAO f,D) by A1, A3, A5, FINSEQ_1:def 3;
then the charact of (FreeUnivAlgZAO f,D) . n = FreeOpZAO n,f,D by Def18;
hence (signature (FreeUnivAlgZAO f,D)) . n = arity h by A5, UNIALG_1:def 11
.= f . n by A6, A7, PARTFUN1:def 8 ;
:: thesis: verum

end;

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