consider f being ManySortedSet of , g being ManySortedSet of such that
A2: X = [f,g] by Def4;
thus for b₁ being B -defined Function st b₁ = X `2 holds
b₁ is total by A2, MCART_1:7; :: thesis: verum