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