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