let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st U1,U2 are_similar holds
for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar implies for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h )
assume A1: U1,U2 are_similar ; :: thesis: for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h
let o be OperSymbol of (MSSign U1); :: thesis: (MSAlg h) . (the_result_sort_of o) = h
set f = MSAlg h;
A2: 0 in {0 } by TARSKI:def 1;
reconsider f1 = (*--> 0 ) * (signature U2) as Function of (dom (signature U2)),({0 } * ) by MSUALG_1:7;
reconsider f2 = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A4: ( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = f2 & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def 13;
consider n being Nat such that
A7: the carrier' of (MSSign U1) = Seg n by MSUALG_1:def 12;
A8: (n |-> 0 ) . o = 0 by A7, FUNCOP_1:13;
thus (MSAlg h) . (the_result_sort_of o) = (MSAlg h) . (the ResultSort of (MSSign U1) . o) by MSUALG_1:def 7
.= (0 .--> h) . 0 by A1, A4, A7, A8, Def3, Th10
.= h by A2, FUNCOP_1:13 ; :: thesis: verum