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 <*1*> ^ (p ^ q) = r => s by FINSEQ_1:32
.= <*1*> ^ (r ^ s) by FINSEQ_1:32 ;
then p ^ q = r ^ s by Th2;
hence ( p = r & s = q ) by Th18; :: thesis: verum