set X = NAT ;
let S be non empty FinSequence of NAT ; ex A being Universal_Algebra st
( the carrier of A = NAT & signature A = S & ( for i, j being Nat st i in dom S & j = S . i holds
the charact of A . i = (j -tuples_on NAT) --> i ) )
A1:
dom S = Seg (len S)
by FINSEQ_1:def 3;
defpred S1[ object , object ] means ex i, j being Element of NAT st
( $1 = i & j = S . i & $2 = (j -tuples_on NAT) --> i );
A2:
for y being object st y in dom S holds
ex z being object st S1[y,z]
consider ch being Function such that
A3:
( dom ch = dom S & ( for y being object st y in dom S holds
S1[y,ch . y] ) )
from CLASSES1:sch 1(A2);
reconsider ch = ch as FinSequence by A1, A3, FINSEQ_1:def 2;
rng ch c= PFuncs ((NAT *),NAT)
then reconsider ch = ch as PFuncFinSequence of NAT by FINSEQ_1:def 4;
set A = UAStr(# NAT,ch #);
A8:
UAStr(# NAT,ch #) is quasi_total
proof
let n be
Nat;
UNIALG_1:def 2,
MARGREL1:def 24 for b1 being Element of bool [:( the carrier of UAStr(# NAT,ch #) *), the carrier of UAStr(# NAT,ch #):] holds
( not n in dom the charact of UAStr(# NAT,ch #) or not b1 = the charact of UAStr(# NAT,ch #) . n or b1 is quasi_total )let h be
PartFunc of
( the carrier of UAStr(# NAT,ch #) *), the
carrier of
UAStr(#
NAT,
ch #);
( not n in dom the charact of UAStr(# NAT,ch #) or not h = the charact of UAStr(# NAT,ch #) . n or h is quasi_total )
assume that A9:
n in dom the
charact of
UAStr(#
NAT,
ch #)
and A10:
h = the
charact of
UAStr(#
NAT,
ch #)
. n
;
h is quasi_total
ex
i,
j being
Element of
NAT st
(
n = i &
j = S . i &
h = (j -tuples_on NAT) --> i )
by A3, A9, A10;
hence
h is
quasi_total
;
verum
end;
A11:
UAStr(# NAT,ch #) is non-empty
UAStr(# NAT,ch #) is partial
proof
let n be
Nat;
UNIALG_1:def 1,
MARGREL1:def 23 for b1 being Element of bool [:( the carrier of UAStr(# NAT,ch #) *), the carrier of UAStr(# NAT,ch #):] holds
( not n in dom the charact of UAStr(# NAT,ch #) or not b1 = the charact of UAStr(# NAT,ch #) . n or b1 is homogeneous )let h be
PartFunc of
( the carrier of UAStr(# NAT,ch #) *), the
carrier of
UAStr(#
NAT,
ch #);
( not n in dom the charact of UAStr(# NAT,ch #) or not h = the charact of UAStr(# NAT,ch #) . n or h is homogeneous )
assume that A14:
n in dom the
charact of
UAStr(#
NAT,
ch #)
and A15:
h = the
charact of
UAStr(#
NAT,
ch #)
. n
;
h is homogeneous
ex
i,
j being
Element of
NAT st
(
n = i &
j = S . i &
h = (j -tuples_on NAT) --> i )
by A3, A14, A15;
hence
h is
homogeneous
;
verum
end;
then reconsider A = UAStr(# NAT,ch #) as Universal_Algebra by A8, A11;
take
A
; ( the carrier of A = NAT & signature A = S & ( for i, j being Nat st i in dom S & j = S . i holds
the charact of A . i = (j -tuples_on NAT) --> i ) )
thus
the carrier of A = NAT
; ( signature A = S & ( for i, j being Nat st i in dom S & j = S . i holds
the charact of A . i = (j -tuples_on NAT) --> i ) )
A16:
len ch = len S
by A3, FINSEQ_3:29;
hence
signature A = S
by A16, UNIALG_1:def 4; for i, j being Nat st i in dom S & j = S . i holds
the charact of A . i = (j -tuples_on NAT) --> i
let i, j be Nat; ( i in dom S & j = S . i implies the charact of A . i = (j -tuples_on NAT) --> i )
assume
i in dom S
; ( not j = S . i or the charact of A . i = (j -tuples_on NAT) --> i )
then
ex i1, j being Element of NAT st
( i = i1 & j = S . i1 & ch . i = (j -tuples_on NAT) --> i1 )
by A3;
hence
( not j = S . i or the charact of A . i = (j -tuples_on NAT) --> i )
; verum