let F, F1, G, G1 be ZF-formula; :: thesis: ( F => G = F1 => G1 implies ( F = F1 & G = G1 ) )
assume F => G = F1 => G1 ; :: thesis: ( F = F1 & G = G1 )
then A1: F '&' ('not' G) = F1 '&' ('not' G1) by FINSEQ_1:33;
hence F = F1 by Th30; :: thesis: G = G1
'not' G = 'not' G1 by A1, Th30;
hence G = G1 by FINSEQ_1:33; :: thesis: verum