theorem Th34: :: HILBERT3:35

for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V holds Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):]