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) 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 A1, A3, 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 and
A5: y = ch . xi by FUNCT_1:def 5;
consider i, j being Nat such that
xi = i and
j = S . i and
A6: y = (j -tuples_on X) --> x by A3, A4, A5;
A7: dom ((j -tuples_on X) --> x) = j -tuples_on X by FUNCOP_1:19;
rng ((j -tuples_on X) --> x) c= {x} by FUNCOP_1:19;
hence not y nin PFuncs (X * ),X by A6, A7, PARTFUN1:def 5; :: thesis: verum

end;

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

proof

let n be Nat; :: according to UNIALG_1:def 8,MARGREL1:def 25 :: 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 that
A9: n in dom the charact of UAStr(# X,ch #) and
A10: h = the charact of UAStr(# X,ch #) . n ; :: thesis: h is quasi_total
ex i, j being Nat st
( n = i & j = S . i & h = (j -tuples_on X) --> x ) by A3, A9, A10;
hence h is quasi_total ; :: thesis: verum

end;

A11: 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
A12: a in dom ch and
A13: {} = ch . a by FUNCT_1:def 5;
ex i, j being Nat st
( a = i & j = S . i & {} = (j -tuples_on X) --> x ) by A3, A12, A13;
hence contradiction ; :: thesis: verum

end;

UAStr(# X,ch #) is partial

proof

let n be Nat; :: according to UNIALG_1:def 7,MARGREL1:def 24 :: 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 that
A14: n in dom the charact of UAStr(# X,ch #) and
A15: h = the charact of UAStr(# X,ch #) . n ; :: thesis: h is homogeneous
ex i, j being Nat st
( n = i & j = S . i & h = (j -tuples_on X) --> x ) by A3, A14, A15;
hence h is homogeneous ; :: thesis: verum

end;

then reconsider A = UAStr(# X,ch #) as Universal_Algebra by A8, A11;
take A ; :: thesis: ( the carrier of A = X & signature A = S )
thus the carrier of A = X ; :: thesis: signature A = S
A16: 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 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 Nat such that
A18: n = i and
A19: j = S . i and
A20: h = (j -tuples_on X) --> x by A3, A17;
consider z being Element of j -tuples_on X;
A21: dom h = j -tuples_on X by A20, FUNCOP_1:19;
len z = j by FINSEQ_1:def 18;
hence S . n = arity h by A18, A19, A21, MARGREL1:def 26; :: thesis: verum

end;

hence signature A = S by A16, UNIALG_1:def 11; :: thesis: verum