set U1 = the Universal_Algebra;

set f = J --> the Universal_Algebra;

reconsider f = J --> the Universal_Algebra as ManySortedSet of J ;

take f ; :: thesis: ( f is equal-signature & f is Univ_Alg-yielding )

for x, y being object 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

thus f is Univ_Alg-yielding by FUNCOP_1:7; :: thesis: verum

set f = J --> the Universal_Algebra;

reconsider f = J --> the Universal_Algebra as ManySortedSet of J ;

take f ; :: thesis: ( f is equal-signature & f is Univ_Alg-yielding )

for x, y being object 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

hence
f is equal-signature
; :: thesis: f is Univ_Alg-yielding
let x, y be object ; :: 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 that

A2: x in dom f and

A3: y in dom f ; :: thesis: for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds

signature U1 = signature U2

let U2, U3 be Universal_Algebra; :: thesis: ( U2 = f . x & U3 = f . y implies signature U2 = signature U3 )

assume A4: ( U2 = f . x & U3 = f . y ) ; :: thesis: signature U2 = signature U3

f . x = the Universal_Algebra by A2, FUNCOP_1:7;

hence signature U2 = signature U3 by A3, A4, FUNCOP_1:7; :: thesis: verum

end;signature U1 = signature U2 )

assume that

A2: x in dom f and

A3: y in dom f ; :: thesis: for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds

signature U1 = signature U2

let U2, U3 be Universal_Algebra; :: thesis: ( U2 = f . x & U3 = f . y implies signature U2 = signature U3 )

assume A4: ( U2 = f . x & U3 = f . y ) ; :: thesis: signature U2 = signature U3

f . x = the Universal_Algebra by A2, FUNCOP_1:7;

hence signature U2 = signature U3 by A3, A4, FUNCOP_1:7; :: thesis: verum

thus f is Univ_Alg-yielding by FUNCOP_1:7; :: thesis: verum