:: deftheorem Def3 defines InducedTarget MSSCYC_2:def 3 :
for S being ManySortedSign
for b₂ being Function of (InducedEdges S), the carrier of S holds
( b₂ = InducedTarget S iff for e being object st e in InducedEdges S holds
b₂ . e = the ResultSort of S . (e `1) );