t . a is Morphism of , by A1, Def2;
hence ex b₁ being Morphism of , st b₁ = t . a ; :: thesis: verum