theorem :: ZF_FUND1:26

for v1, v2 being Element of VAR holds
( code {v1} = {(x". v1)} & code {v1,v2} = {(x". v1),(x". v2)} ) by Lm6, Lm7;