consider U1 being Universal_Algebra;
set f = J --> U1;
A1: dom (J --> U1) = J by FUNCOP_1:19;
then reconsider f = J --> U1 as ManySortedSet of by PARTFUN1:def 4;
take f ; :: thesis: ( f is equal-signature & f is Univ_Alg-yielding )
for x, y being set st x in dom f & y in dom f holds
for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds
signature U1 = signature U2

proof

let x, y be set ; :: thesis: ( x in dom f & y in dom f implies for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds
signature U1 = signature U2 )
assume ( x in dom f & y in dom f ) ; :: thesis: for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds
signature U1 = signature U2
then A2: ( f . x = U1 & f . y = U1 ) by A1, FUNCOP_1:13;
let U2, U3 be Universal_Algebra; :: thesis: ( U2 = f . x & U3 = f . y implies signature U2 = signature U3 )
assume ( U2 = f . x & U3 = f . y ) ; :: thesis: signature U2 = signature U3
hence signature U2 = signature U3 by A2; :: thesis: verum

end;

hence f is equal-signature by Def12; :: thesis: f is Univ_Alg-yielding
for x being set st x in dom f holds
f . x is Universal_Algebra by A1, FUNCOP_1:13;
hence f is Univ_Alg-yielding by Def10; :: thesis: verum