let f be non empty FinSequence of NAT ; for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f
let D be non empty disjoint_with_NAT set ; 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 for n being Nat st n in dom (signature (FreeUnivAlgNSG (f,D))) holds
(signature (FreeUnivAlgNSG (f,D))) . n = f . nlet n be
Nat;
( 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)))
;
(signature (FreeUnivAlgNSG (f,D))) . n = f . nthen 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
;
verum end;
hence
signature (FreeUnivAlgNSG (f,D)) = f
by A2, A1, FINSEQ_2:9; verum