theorem :: ZF_FUND1:34

for A, B being finite Subset of VAR holds
( code (A \/ B) = (code A) \/ (code B) & code (A \ B) = (code A) \ (code B) ) by Lm1, FUNCT_1:64, RELAT_1:120;