let S be non empty FinSequence of NAT ; :: thesis:
let i, j be Nat; :: thesis:
reconsider j' = j as Element of NAT by ORDINAL1:def 13;
assume A1: ( i in dom S & j = S . i ) ; :: thesis:
let X be non empty set ; :: thesis:
consider A0 being Universal_Algebra such that
A2: ( the carrier of A0 = X & signature A0 = S ) by Th13;
let f be Function of j -tuples_on X,X; :: thesis:
j' -tuples_on X c= X * by CATALG_1:6;
then reconsider f0 = f as PartFunc of X * ,X by RELSET_1:17;
consider z being Element of j -tuples_on X;
A3: dom f0 = j -tuples_on X by FUNCT_2:def 1;
f0 is homogeneous

let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis:
assume ( x in dom f0 & y in dom f0 ) ; :: thesis:
then ( len x = j & len y = j ) by A3, FINSEQ_2:109;
hence len x = len y ; :: thesis:

end;

then reconsider f0 = f0 as non empty homogeneous PartFunc of X * ,X ;
A4: len z = j by FINSEQ_2:109;
then A5: arity f0 = j by A3, UNIALG_1:def 10;
set ch = the charact of A0 +* i,f0;
f0 in PFuncs (X * ),X by PARTFUN1:119;
then ( {f0} c= PFuncs (X * ),X & rng the charact of A0 c= PFuncs (X * ),X ) by A2, ZFMISC_1:37;
then ( rng (the charact of A0 +* i,f0) c= (rng the charact of A0) \/ {f0} & (rng the charact of A0) \/ {f0} c= PFuncs (X * ),X ) by FUNCT_7:102, XBOOLE_1:8;
then rng (the charact of A0 +* i,f0) c= PFuncs (X * ),X by XBOOLE_1:1;
then reconsider ch = the charact of A0 +* i,f0 as FinSequence of PFuncs (X * ),X by FINSEQ_1:def 4;
A6: dom ch = dom the charact of A0 by FUNCT_7:32;
set A = UAStr(# X,ch #);
A7: UAStr(# X,ch #) is quasi_total

let n be Nat; :: according to UNIALG_1:def 5,UNIALG_1:def 8 :: thesis:
let h be PartFunc of the carrier of UAStr(# X,ch #) * ,the carrier of UAStr(# X,ch #); :: thesis:
assume A8: ( n in dom the charact of UAStr(# X,ch #) & h = the charact of UAStr(# X,ch #) . n ) ; :: thesis:
then ( ( n = i implies h = f0 ) & ( n <> i implies h = the charact of A0 . n ) & the charact of A0 is quasi_total ) by A6, FUNCT_7:33, FUNCT_7:34;
hence h is quasi_total by A2, A5, A3, A8, A6, COMPUT_1:25, UNIALG_1:def 5; :: thesis:

end;

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

thus the charact of UAStr(# X,ch #) <> {} by A6; :: according to UNIALG_1:def 9 :: thesis:
assume {} in rng the charact of UAStr(# X,ch #) ; :: according to RELAT_1:def 9 :: thesis:
then consider a being set such that
A10: ( a in dom ch & {} = ch . a ) by FUNCT_1:def 5;
reconsider a = a as Element of NAT by A10;
( ( a = i implies {} = f0 ) & ( a <> i implies {} = the charact of A0 . a ) & {} nin rng the charact of A0 ) by A10, A6, FUNCT_7:33, FUNCT_7:34, RELAT_1:def 9;
hence contradiction by A6, A10; :: thesis:

end;

UAStr(# X,ch #) is partial

let n be Nat; :: according to UNIALG_1:def 4,UNIALG_1:def 7 :: thesis:
let h be PartFunc of the carrier of UAStr(# X,ch #) * ,the carrier of UAStr(# X,ch #); :: thesis:
assume ( n in dom the charact of UAStr(# X,ch #) & h = the charact of UAStr(# X,ch #) . n ) ; :: thesis:
then ( ( n = i implies h = f0 ) & ( n <> i implies h = the charact of A0 . n ) & the charact of A0 is homogeneous ) by A6, FUNCT_7:33, FUNCT_7:34;
hence h is homogeneous ; :: thesis:

end;

then reconsider A = UAStr(# X,ch #) as Universal_Algebra by A7, A9;
take A ; :: thesis:
thus the carrier of A = X ; :: thesis:
A11: len S = len the charact of A0 by A2, UNIALG_1:def 11;
then A12: dom S = dom the charact of A0 by FINSEQ_3:31;
A13: len S = len the charact of A by A11, A6, FINSEQ_3:31;

let n be Nat; :: thesis:
assume A14: n in dom S ; :: thesis:
let h be non empty homogeneous PartFunc of the carrier of A * ,the carrier of A; :: thesis:
assume h = the charact of A . n ; :: thesis:
then ( ( n = i implies h = f0 ) & ( n <> i implies h = the charact of A0 . n ) ) by A12, A14, FUNCT_7:33, FUNCT_7:34;
hence S . n = arity h by A2, A1, A14, A4, A3, UNIALG_1:def 10, UNIALG_1:def 11; :: thesis:

end;

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