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

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