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