:: deftheorem Def11 defines fComp ENS_1:def 11 :
for V being non empty set
for b₂ being PartFunc of [:(Maps V),(Maps V):],(Maps V) holds
( b₂ = fComp V iff ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₂ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₂ . [m2,m1] = m2 * m1 ) ) );