let p, q, r, s be Element of HP-WFF ; :: thesis: ( p '&' q = r '&' s implies ( p = r & s = q ) )
assume p '&' q = r '&' s ; :: thesis: ( p = r & s = q )
then <*2*> ^ (p ^ q) = r '&' s by FINSEQ_1:32
.= <*2*> ^ (r ^ s) by FINSEQ_1:32 ;
then p ^ q = r ^ s by Th2;
hence ( p = r & s = q ) by Th18; :: thesis: verum