dom h = I by PARTFUN1:def 2;
hence ex b₁ being Homomorphism of (dsum N),(sum M) st
( b₁ = SumMap ((sum_bundle N),M,h) & b₁ is bijective ) by A2, GROUP_19:41; :: thesis: verum