let X be non empty set ; :: thesis: for S being non empty FinSequence of NAT ex A being Universal_Algebra st
( the carrier of A = X & signature A = S )
let S be non empty FinSequence of NAT ; :: thesis: ex A being Universal_Algebra st
( the carrier of A = X & signature A = S )
A1: ( dom S = Seg (len S) & rng S c= NAT ) by FINSEQ_1:def 3;
consider x being Element of X;
defpred S₁[ set , set ] means ex i, j being Nat st
( $1 = i & j = S . i & $2 = (j -tuples_on X) --> x );
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 X) --> x; :: thesis: S₁[y,z]
take i ; :: thesis: ex j being Nat st
( y = i & j = S . i & z = (j -tuples_on X) --> x )
take j ; :: thesis: ( y = i & j = S . i & z = (j -tuples_on X) --> x )
thus ( y = i & j = S . i & z = (j -tuples_on X) --> x ) ; :: 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 (X * ),X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( y nin rng ch or not y nin PFuncs (X * ),X )
assume y in rng ch ; :: thesis: not y nin PFuncs (X * ),X
then consider xi being set such that
A4: ( xi in dom ch & y = ch . xi ) by FUNCT_1:def 5;
consider i, j being Nat such that
A5: ( xi = i & j = S . i & y = (j -tuples_on X) --> x ) by A3, A4;
( dom ((j -tuples_on X) --> x) = j -tuples_on X & rng ((j -tuples_on X) --> x) c= {x} ) by FUNCOP_1:19;
hence not y nin PFuncs (X * ),X by A5, PARTFUN1:def 5; :: thesis: verum

end;

then reconsider ch = ch as PFuncFinSequence of X by FINSEQ_1:def 4;
set A = UAStr(# X,ch #);
A6: UAStr(# X,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(# X,ch #) * ),the carrier of UAStr(# X,ch #):] holds
( n nin dom the charact of UAStr(# X,ch #) or not b₁ = the charact of UAStr(# X,ch #) . n or b₁ is quasi_total )
let h be PartFunc of (the carrier of UAStr(# X,ch #) * ),the carrier of UAStr(# X,ch #); :: thesis: ( n nin dom the charact of UAStr(# X,ch #) or not h = the charact of UAStr(# X,ch #) . n or h is quasi_total )
assume ( n in dom the charact of UAStr(# X,ch #) & h = the charact of UAStr(# X,ch #) . n ) ; :: thesis: h is quasi_total
then ex i, j being Nat st
( n = i & j = S . i & h = (j -tuples_on X) --> x ) by A3;
hence h is quasi_total ; :: thesis: verum

end;

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

proof

thus the charact of UAStr(# X,ch #) <> {} by A3; :: according to UNIALG_1:def 9 :: thesis: the charact of UAStr(# X,ch #) is non-empty
assume {} in rng the charact of UAStr(# X,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 Nat st
( a = i & j = S . i & {} = (j -tuples_on X) --> x ) by A8, A3;
hence contradiction ; :: thesis: verum

end;

UAStr(# X,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(# X,ch #) * ),the carrier of UAStr(# X,ch #):] holds
( n nin dom the charact of UAStr(# X,ch #) or not b₁ = the charact of UAStr(# X,ch #) . n or b₁ is homogeneous )
let h be PartFunc of (the carrier of UAStr(# X,ch #) * ),the carrier of UAStr(# X,ch #); :: thesis: ( n nin dom the charact of UAStr(# X,ch #) or not h = the charact of UAStr(# X,ch #) . n or h is homogeneous )
assume ( n in dom the charact of UAStr(# X,ch #) & h = the charact of UAStr(# X,ch #) . n ) ; :: thesis: h is homogeneous
then ex i, j being Nat st
( n = i & j = S . i & h = (j -tuples_on X) --> x ) by A3;
hence h is homogeneous ; :: thesis: verum

end;

then reconsider A = UAStr(# X,ch #) as Universal_Algebra by A6, A7;
take A ; :: thesis: ( the carrier of A = X & signature A = S )
thus the carrier of A = X ; :: thesis: signature A = S
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 Nat such that
A11: ( n = i & j = S . i & h = (j -tuples_on X) --> x ) by A3, A10;
consider z being Element of j -tuples_on X;
( dom h = j -tuples_on X & 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: verum