let p, q be Element of HP-WFF ; :: thesis: for V being SetValuation
for P being Permutation of V holds Perm P,(p '&' q) = [:(Perm P,p),(Perm P,q):]
let V be SetValuation; :: thesis: for P being Permutation of V holds Perm P,(p '&' q) = [:(Perm P,p),(Perm P,q):]
let P be Permutation of V; :: thesis: Perm P,(p '&' q) = [:(Perm P,p),(Perm P,q):]
ex p' being Permutation of (SetVal V,p) ex q' being Permutation of (SetVal V,q) st
( p' = (Perm P) . p & q' = (Perm P) . q & (Perm P) . (p '&' q) = [:p',q':] & (Perm P) . (p => q) = p' => q' ) by Def5;
hence Perm P,(p '&' q) = [:(Perm P,p),(Perm P,q):] ; :: thesis: verum