let o be operation of S; :: thesis: o is homogeneous
consider i being object such that
A1: ( i in dom the charact of S & o = the charact of S . i ) by FUNCT_1:def 3;
thus o is homogeneous by A1; :: thesis: verum