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 p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = (Perm P) . p & q9 = (Perm P) . q & (Perm P) . (p '&' q) = [:p9,q9:] & (Perm P) . (p => q) = p9 => q9 ) by Def5;

hence Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] ; :: thesis: verum

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 p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = (Perm P) . p & q9 = (Perm P) . q & (Perm P) . (p '&' q) = [:p9,q9:] & (Perm P) . (p => q) = p9 => q9 ) by Def5;

hence Perm (P,(p '&' q)) = [:(Perm (P,p)),(Perm (P,q)):] ; :: thesis: verum