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) & rng S c= NAT ) by FINSEQ_1:def 3;
defpred S₁[ set , set ] means ex i, j being Element of NAT st
( $1 = i & j = S . i & $2 = (j -tuples_on NAT ) --> i );
A2: for y being set st y in dom S holds
ex z being set st S₁[y,z]

proof

let y be set ; :: thesis: ( y in dom S implies ex z being set st S₁[y,z] )
assume y in dom S ; :: thesis: ex z being set st S₁[y,z]
then reconsider i = y as Element of NAT ;
reconsider j = S . i as Element of NAT ;
take z = (j -tuples_on NAT ) --> i; :: thesis: S₁[y,z]
take i ; :: thesis: ex j being Element of NAT st
( y = i & j = S . i & z = (j -tuples_on NAT ) --> i )
take j ; :: thesis: ( y = i & j = S . i & z = (j -tuples_on NAT ) --> i )
thus ( y = i & j = S . i & z = (j -tuples_on NAT ) --> i ) ; :: thesis: verum

end;

consider ch being Function such that
A3: ( dom ch = dom S & ( for y being set st y in dom S holds
S₁[y,ch . y] ) ) from CLASSES1:sch 1(A2);
reconsider ch = ch as FinSequence by A3, A1, FINSEQ_1:def 2;
rng ch c= PFuncs (NAT * ),NAT

proof

let y be set ; :: 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 set such that
A4: ( xi in dom ch & y = ch . xi ) by FUNCT_1:def 5;
consider i, j being Element of NAT such that
A5: ( xi = i & j = S . i & y = (j -tuples_on NAT ) --> i ) by A3, A4;
( dom ((j -tuples_on NAT ) --> i) = j -tuples_on NAT & rng ((j -tuples_on NAT ) --> i) c= {i} ) by FUNCOP_1:19;
hence not y nin PFuncs (NAT * ),NAT by A5, PARTFUN1:def 5; :: thesis: verum

end;

then reconsider ch = ch as PFuncFinSequence of NAT by FINSEQ_1:def 4;
set A = UAStr(# NAT ,ch #);
A6: UAStr(# NAT ,ch #) is quasi_total

proof

let n be Nat; :: according to UNIALG_1:def 5,UNIALG_1:def 8 :: thesis: for b₁ being Element of bool [:(the carrier of UAStr(# NAT ,ch #) * ),the carrier of UAStr(# NAT ,ch #):] holds
( n nin dom the charact of UAStr(# NAT ,ch #) or not b₁ = the charact of UAStr(# NAT ,ch #) . n or b₁ is quasi_total )
let h be PartFunc of (the carrier of UAStr(# NAT ,ch #) * ),the carrier of UAStr(# NAT ,ch #); :: thesis: ( n nin dom the charact of UAStr(# NAT ,ch #) or not h = the charact of UAStr(# NAT ,ch #) . n or h is quasi_total )
assume ( n in dom the charact of UAStr(# NAT ,ch #) & h = the charact of UAStr(# NAT ,ch #) . n ) ; :: thesis: h is quasi_total
then ex i, j being Element of NAT st
( n = i & j = S . i & h = (j -tuples_on NAT ) --> i ) by A3;
hence h is quasi_total ; :: thesis: verum

end;

A7: UAStr(# NAT ,ch #) is non-empty

proof

thus the charact of UAStr(# NAT ,ch #) <> {} by A3; :: according to UNIALG_1:def 9 :: 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 set such that
A8: ( a in dom ch & {} = ch . a ) by FUNCT_1:def 5;
ex i, j being Element of NAT st
( a = i & j = S . i & {} = (j -tuples_on NAT ) --> i ) by A8, A3;
hence contradiction ; :: thesis: verum

end;

UAStr(# NAT ,ch #) is partial

proof

let n be Nat; :: according to UNIALG_1:def 4,UNIALG_1:def 7 :: thesis: for b₁ being Element of bool [:(the carrier of UAStr(# NAT ,ch #) * ),the carrier of UAStr(# NAT ,ch #):] holds
( n nin dom the charact of UAStr(# NAT ,ch #) or not b₁ = the charact of UAStr(# NAT ,ch #) . n or b₁ is homogeneous )
let h be PartFunc of (the carrier of UAStr(# NAT ,ch #) * ),the carrier of UAStr(# NAT ,ch #); :: thesis: ( n nin dom the charact of UAStr(# NAT ,ch #) or not h = the charact of UAStr(# NAT ,ch #) . n or h is homogeneous )
assume ( n in dom the charact of UAStr(# NAT ,ch #) & h = the charact of UAStr(# NAT ,ch #) . n ) ; :: thesis: h is homogeneous
then ex i, j being Element of NAT st
( n = i & j = S . i & h = (j -tuples_on NAT ) --> i ) by A3;
hence h is homogeneous ; :: thesis: verum

end;

then reconsider A = UAStr(# NAT ,ch #) as Universal_Algebra by A6, A7;
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 ) )
A9: len ch = len S by A3, FINSEQ_3:31;

now

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 A10: 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
A11: ( n = i & j = S . i & h = (j -tuples_on NAT ) --> i ) by A3, A10;
consider z being Element of j -tuples_on NAT ;
( dom h = j -tuples_on NAT & len z = j ) by A11, FINSEQ_1:def 18, FUNCOP_1:19;
hence S . n = arity h by A11, UNIALG_1:def 10; :: thesis: verum

end;

hence signature A = S by A9, UNIALG_1:def 11; :: 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
consider A being Universal_Algebra;
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