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