:: deftheorem Def2 defines InducedSource MSSCYC_2:def 2 :
for S being ManySortedSign
for b₂ being Function of (InducedEdges S), the carrier of S holds
( b₂ = InducedSource S iff for e being object st e in InducedEdges S holds
b₂ . e = e `2 );