set X = NAT ;
let S be non empty FinSequence of NAT ; :: thesis: 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]
proof
let y be object ; :: thesis: ( y in dom S implies ex z being object st S1[y,z] )
assume y in dom S ; :: thesis: ex z being object st S1[y,z]
then reconsider i = y as Element of NAT ;
reconsider j = S . i as Element of NAT ;
take (j -tuples_on NAT) --> i ; :: thesis: S1[y,(j -tuples_on NAT) --> i]
take i ; :: thesis: ex j being Element of NAT st
( y = i & j = S . i & (j -tuples_on NAT) --> i = (j -tuples_on NAT) --> i )
take j ; :: thesis: ( y = i & j = S . i & (j -tuples_on NAT) --> i = (j -tuples_on NAT) --> i )
thus ( y = i & j = S . i & (j -tuples_on NAT) --> i = (j -tuples_on NAT) --> i ) ; :: thesis: verum
end;
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)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( y nin rng ch or not y nin PFuncs ((NAT *),NAT) )
assume y in rng ch ; :: thesis: not y nin PFuncs ((NAT *),NAT)
then consider xi being object such that
A4: xi in dom ch and
A5: y = ch . xi by FUNCT_1:def 3;
consider i, j being Element of NAT such that
xi = i and
j = S . i and
A6: y = (j -tuples_on NAT) --> i by A3, A4, A5;
A7: dom ((j -tuples_on NAT) --> i) = j -tuples_on NAT by FUNCOP_1:13;
rng ((j -tuples_on NAT) --> i) c= NAT ;
hence not y nin PFuncs ((NAT *),NAT) by A6, A7, PARTFUN1:def 3; :: thesis: verum
end;
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; :: according to UNIALG_1:def 2,MARGREL1:def 24 :: thesis: 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 #); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum
end;
A11: UAStr(# NAT,ch #) is non-empty
proof
thus the charact of UAStr(# NAT,ch #) <> {} by A3; :: according to UNIALG_1:def 3 :: thesis: the charact of UAStr(# NAT,ch #) is non-empty
assume {} in rng the charact of UAStr(# NAT,ch #) ; :: according to RELAT_1:def 9 :: thesis: contradiction
then consider a being object such that
A12: a in dom ch and
A13: {} = ch . a by FUNCT_1:def 3;
ex i, j being Element of NAT st
( a = i & j = S . i & {} = (j -tuples_on NAT) --> i ) by A3, A12, A13;
hence contradiction ; :: thesis: verum
end;
UAStr(# NAT,ch #) is partial
proof
let n be Nat; :: according to UNIALG_1:def 1,MARGREL1:def 23 :: thesis: 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 #); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum
end;
then reconsider A = UAStr(# NAT,ch #) as Universal_Algebra by A8, A11;
take A ; :: thesis: ( 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 ; :: thesis: ( 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;
now :: thesis: for n being Nat st n in dom S holds
for h being non empty homogeneous PartFunc of ( the carrier of A *), the carrier of A st h = the charact of A . n holds
S . n = arity h
let n be Nat; :: thesis: ( n in dom S implies for h being non empty homogeneous PartFunc of ( the carrier of A *), the carrier of A st h = the charact of A . n holds
S . n = arity h )
assume A17: n in dom S ; :: thesis: for h being non empty homogeneous PartFunc of ( the carrier of A *), the carrier of A st h = the charact of A . n holds
S . n = arity h
let h be non empty homogeneous PartFunc of ( the carrier of A *), the carrier of A; :: thesis: ( h = the charact of A . n implies S . n = arity h )
assume h = the charact of A . n ; :: thesis: S . n = arity h
then consider i, j being Element of NAT such that
A18: n = i and
A19: j = S . i and
A20: h = (j -tuples_on NAT) --> i by A3, A17;
set z = the Element of j -tuples_on NAT;
A21: dom h = j -tuples_on NAT by A20, FUNCOP_1:13;
len the Element of j -tuples_on NAT = j by CARD_1:def 7;
hence S . n = arity h by A18, A19, A21, MARGREL1:def 25; :: thesis: verum
end;
hence signature A = S by A16, UNIALG_1:def 4; :: thesis: 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; :: thesis: ( i in dom S & j = S . i implies the charact of A . i = (j -tuples_on NAT) --> i )
assume i in dom S ; :: thesis: ( 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 ) ; :: thesis: verum