set H = SumMap ((sum_bundle N),M,h);
A3: dom h = I by PARTFUN1:def 2;
for i being object st i in I holds
ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = h . i & hi is bijective ) by A2;
hence ex b₁ being Homomorphism of (dsum N),(sum M) st
( b₁ = SumMap ((sum_bundle N),M,h) & b₁ is bijective ) by A3, GROUP_19:41; :: thesis: verum