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;
set x = the Element of X;
defpred S₁[ object , object ] means ex i, j being Nat st
( $1 = i & j = S . i & $2 = (j -tuples_on X) --> the Element of X );
A2: for y being object st y in dom S holds
ex z being object st S₁[y,z]

proof

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

end;

consider ch being Function such that
A3: ( dom ch = dom S & ( for y being object 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 object ; :: 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 object such that
A4: xi in dom ch and
A5: y = ch . xi by FUNCT_1:def 3;
consider i, j being Nat such that
xi = i and
j = S . i and
A6: y = (j -tuples_on X) --> the Element of X by A3, A4, A5;
A7: dom ((j -tuples_on X) --> the Element of X) = j -tuples_on X by FUNCOP_1:13;
rng ((j -tuples_on X) --> the Element of X) c= { the Element of X} by FUNCOP_1:13;
hence not y nin PFuncs ((X *),X) by A6, A7, PARTFUN1:def 3; :: 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 2,MARGREL1:def 24 :: thesis: for b₁ being Element of bool [:( the carrier of UAStr(# X,ch #) *), the carrier of UAStr(# X,ch #):] holds
( not n in 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: ( not n in 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) --> the Element of 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 3 :: 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 object such that
A12: a in dom ch and
A13: {} = ch . a by FUNCT_1:def 3;
ex i, j being Nat st
( a = i & j = S . i & {} = (j -tuples_on X) --> the Element of 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 1,MARGREL1:def 23 :: thesis: for b₁ being Element of bool [:( the carrier of UAStr(# X,ch #) *), the carrier of UAStr(# X,ch #):] holds
( not n in 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: ( not n in 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) --> the Element of 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: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 Nat such that
A18: n = i and
A19: j = S . i and
A20: h = (j -tuples_on X) --> the Element of X by A3, A17;
set z = the Element of j -tuples_on X;
A21: dom h = j -tuples_on X by A20, FUNCOP_1:13;
len the Element of j -tuples_on X = 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: verum