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 Def17;
A2: len (signature (FreeUnivAlgZAO (f,D))) = len the charact of (FreeUnivAlgZAO (f,D)) by UNIALG_1:def 4;
then A3: dom (signature (FreeUnivAlgZAO (f,D))) = Seg (len f) by A1, FINSEQ_1:def 3;

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

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 MARGREL1:22;
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 Def16;
then A7: arity h = f /. n by A4, FINSEQ_2:110;
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 Def17;
hence (signature (FreeUnivAlgZAO (f,D))) . n = arity h by A5, UNIALG_1:def 4
.= f . n by A6, A7, PARTFUN1:def 6 ;
:: thesis: verum

end;

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