reconsider x = Head s as Element of INT ;
the Tran of T . [(s `1),((s `3) . x)] is Tran-Goal of T ;
hence the Tran of T . [(s `1),((s `3) . (Head s))] is Tran-Goal of T ; :: thesis: verum