reconsider t9 = t as c-Term of A,V by A1, MSATERM:27;
t9 @ f = t9 @ f ;
hence ( ex b₁ being set ex t9 being c-Term of A,V st
( t9 = t & b₁ = t9 @ f ) & ( for b₁, b₂ being set st ex t9 being c-Term of A,V st
( t9 = t & b₁ = t9 @ f ) & ex t9 being c-Term of A,V st
( t9 = t & b₂ = t9 @ f ) holds
b₁ = b₂ ) ) ; :: thesis: verum