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 12;
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:134;
then reconsider f0 = f as PartFunc of (X *),X by RELSET_1:7;
set z = the Element of j -tuples_on X;
A5: dom f0 = j -tuples_on X by FUNCT_2:def 1;
f0 is homogeneous by A5;
then reconsider f0 = f0 as non empty homogeneous PartFunc of (X *),X ;
A6: len the Element of j -tuples_on X = j by CARD_1:def 7;
then A7: arity f0 = j by A5, MARGREL1:def 25;
set ch = the charact of A0 +* (i,f0);
f0 in PFuncs ((X *),X) by PARTFUN1:45;
then A8: {f0} c= PFuncs ((X *),X) by ZFMISC_1:31;
A9: rng ( the charact of A0 +* (i,f0)) c= (rng the charact of A0) \/ {f0} by FUNCT_7:100;
(rng the charact of A0) \/ {f0} c= PFuncs ((X *),X) by A3, A8, XBOOLE_1:8;
then rng ( the charact of A0 +* (i,f0)) c= PFuncs ((X *),X) by A9;
then reconsider ch = the charact of A0 +* (i,f0) as FinSequence of PFuncs ((X *),X) by FINSEQ_1:def 4;
A10: dom ch = dom the charact of A0 by FUNCT_7:30;
set A = UAStr(# X,ch #);
A11: UAStr(# X,ch #) is quasi_total
proof
let n be Nat; :: according to UNIALG_1:def 2,MARGREL1:def 24 :: thesis: for b1 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 b1 = the charact of UAStr(# X,ch #) . n or b1 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
A12: n in dom the charact of UAStr(# X,ch #) and
A13: h = the charact of UAStr(# X,ch #) . n ; :: thesis: h is quasi_total
A14: ( n = i implies h = f0 ) by A10, A12, A13, FUNCT_7:31;
( n <> i implies h = the charact of A0 . n ) by A13, FUNCT_7:32;
hence h is quasi_total by A3, A5, A7, A10, A12, A14, COMPUT_1:22, MARGREL1:def 24; :: thesis: verum
end;
A15: UAStr(# X,ch #) is non-empty
proof
thus the charact of UAStr(# X,ch #) <> {} ; :: 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
A16: a in dom ch and
A17: {} = ch . a by FUNCT_1:def 3;
reconsider a = a as Element of NAT by A16;
( a <> i implies {} = the charact of A0 . a ) by A17, FUNCT_7:32;
hence contradiction by A10, A16, A17, FUNCT_7:31; :: thesis: verum
end;
UAStr(# X,ch #) is partial
proof
let n be Nat; :: according to UNIALG_1:def 1,MARGREL1:def 23 :: thesis: for b1 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 b1 = the charact of UAStr(# X,ch #) . n or b1 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
A18: n in dom the charact of UAStr(# X,ch #) and
A19: h = the charact of UAStr(# X,ch #) . n ; :: thesis: h is homogeneous
( n <> i implies h = the charact of A0 . n ) by A19, FUNCT_7:32;
hence h is homogeneous by A10, A18, A19, FUNCT_7:31; :: thesis: verum
end;
then reconsider A = UAStr(# X,ch #) as Universal_Algebra by A11, A15;
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 )
A20: len S = len the charact of A0 by A4, UNIALG_1:def 4;
then A21: dom S = dom the charact of A0 by FINSEQ_3:29;
A22: len S = len the charact of A by A10, A20, 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 A23: 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 A24: h = the charact of A . n ; :: thesis: S . n = arity h
then A25: ( n = i implies h = f0 ) by A21, A23, FUNCT_7:31;
( n <> i implies h = the charact of A0 . n ) by A24, FUNCT_7:32;
hence S . n = arity h by A2, A4, A5, A6, A23, A25, MARGREL1:def 25, UNIALG_1:def 4; :: thesis: verum
end;
hence signature A = S by A22, UNIALG_1:def 4; :: thesis: the charact of A . i = f
thus the charact of A . i = f by A1, A21, FUNCT_7:31; :: thesis: verum