let UA be Universal_Algebra; :: thesis: for f being Element of UAAut UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
let f be Element of UAAut UA; :: thesis: 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA)
MSAlg f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:9;
hence 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:def 3; :: thesis: verum