let S be non empty FinSequence of NAT ; :: thesis: for i, j being Nat st i in dom S & j = S . i holds
for X being non empty set
for f being Function of (j -tuples_on X),X ex A being Universal_Algebra st
( the carrier of A = X & signature A = S & the charact of A . i = f )
let i, j be Nat; :: thesis: ( i in dom S & j = S . i implies for X being non empty set
for f being Function of (j -tuples_on X),X ex A being Universal_Algebra st
( the carrier of A = X & signature A = S & the charact of A . i = f ) )
reconsider j9 = j as Element of NAT by ORDINAL1:def 13;
assume that
A1: i in dom S and
A2: j = S . i ; :: thesis: for X being non empty set
for f being Function of (j -tuples_on X),X ex A being Universal_Algebra st
( the carrier of A = X & signature A = S & the charact of A . i = f )
let X be non empty set ; :: thesis: for f being Function of (j -tuples_on X),X ex A being Universal_Algebra st
( the carrier of A = X & signature A = S & the charact of A . i = f )
consider A0 being Universal_Algebra such that
A3: the carrier of A0 = X and
A4: signature A0 = S by Th13;
let f be Function of (j -tuples_on X),X; :: thesis: ex A being Universal_Algebra st
( the carrier of A = X & signature A = S & the charact of A . i = f )
j9 -tuples_on X c= X * by FINSEQ_2:154;
then reconsider f0 = f as PartFunc of (X * ),X by RELSET_1:17;
consider z being Element of j -tuples_on X;
A5: dom f0 = j -tuples_on X by FUNCT_2:def 1;
f0 is homogeneous

proof

thus dom f0 is with_common_domain by A5; :: according to MARGREL1:def 22 :: thesis: verum

end;

then reconsider f0 = f0 as non empty homogeneous PartFunc of (X * ),X ;
A8: len z = j by FINSEQ_1:def 18;
then A9: arity f0 = j by A5, MARGREL1:def 26;
set ch = the charact of A0 +* i,f0;
f0 in PFuncs (X * ),X by PARTFUN1:119;
then A10: {f0} c= PFuncs (X * ),X by ZFMISC_1:37;
A11: rng (the charact of A0 +* i,f0) c= (rng the charact of A0) \/ {f0} by FUNCT_7:102;
(rng the charact of A0) \/ {f0} c= PFuncs (X * ),X by A3, A10, XBOOLE_1:8;
then rng (the charact of A0 +* i,f0) c= PFuncs (X * ),X by A11, XBOOLE_1:1;
then reconsider ch = the charact of A0 +* i,f0 as FinSequence of PFuncs (X * ),X by FINSEQ_1:def 4;
A12: dom ch = dom the charact of A0 by FUNCT_7:32;
set A = UAStr(# X,ch #);
A13: 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
A14: n in dom the charact of UAStr(# X,ch #) and
A15: h = the charact of UAStr(# X,ch #) . n ; :: thesis: h is quasi_total
A16: ( n = i implies h = f0 ) by A12, A14, A15, FUNCT_7:33;
( n <> i implies h = the charact of A0 . n ) by A15, FUNCT_7:34;
hence h is quasi_total by A3, A5, A9, A12, A14, A16, COMPUT_1:25, MARGREL1:def 25; :: thesis: verum

end;

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

proof

thus the charact of UAStr(# X,ch #) <> {} by A12; :: 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
A18: a in dom ch and
A19: {} = ch . a by FUNCT_1:def 5;
reconsider a = a as Element of NAT by A18;
( a <> i implies {} = the charact of A0 . a ) by A19, FUNCT_7:34;
hence contradiction by A12, A18, A19, FUNCT_7:33; :: 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
A20: n in dom the charact of UAStr(# X,ch #) and
A21: h = the charact of UAStr(# X,ch #) . n ; :: thesis: h is homogeneous
( n <> i implies h = the charact of A0 . n ) by A21, FUNCT_7:34;
hence h is homogeneous by A12, A20, A21, FUNCT_7:33; :: thesis: verum

end;

then reconsider A = UAStr(# X,ch #) as Universal_Algebra by A13, A17;
take A ; :: thesis: ( the carrier of A = X & signature A = S & the charact of A . i = f )
thus the carrier of A = X ; :: thesis: ( signature A = S & the charact of A . i = f )
A22: len S = len the charact of A0 by A4, UNIALG_1:def 11;
then A23: dom S = dom the charact of A0 by FINSEQ_3:31;
A24: len S = len the charact of A by A12, A22, 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 A25: 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 A26: h = the charact of A . n ; :: thesis: S . n = arity h
then A27: ( n = i implies h = f0 ) by A23, A25, FUNCT_7:33;
( n <> i implies h = the charact of A0 . n ) by A26, FUNCT_7:34;
hence S . n = arity h by A2, A3, A4, A5, A8, A25, A27, MARGREL1:def 26, UNIALG_1:def 11; :: thesis: verum

end;

hence signature A = S by A24, UNIALG_1:def 11; :: thesis: the charact of A . i = f
thus the charact of A . i = f by A1, A23, FUNCT_7:33; :: thesis: verum