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