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
proof
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;
hence f is equal-signature ; :: thesis: f is Univ_Alg-yielding
thus f is Univ_Alg-yielding by FUNCOP_1:7; :: thesis: verum