let p, q be Element of HP-WFF ; :: thesis: for V being SetValuation
for P being Permutation of V
for p' being Permutation of SetVal V,p
for q' being Permutation of SetVal V,q st p' = Perm P,p & q' = Perm P,q holds
Perm P,(p => q) = p' => q'
let V be SetValuation; :: thesis: for P being Permutation of V
for p' being Permutation of SetVal V,p
for q' being Permutation of SetVal V,q st p' = Perm P,p & q' = Perm P,q holds
Perm P,(p => q) = p' => q'
let P be Permutation of V; :: thesis: for p' being Permutation of SetVal V,p
for q' being Permutation of SetVal V,q st p' = Perm P,p & q' = Perm P,q holds
Perm P,(p => q) = p' => q'
A1: 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;
let p' be Permutation of SetVal V,p; :: thesis: for q' being Permutation of SetVal V,q st p' = Perm P,p & q' = Perm P,q holds
Perm P,(p => q) = p' => q'
let q' be Permutation of SetVal V,q; :: thesis: ( p' = Perm P,p & q' = Perm P,q implies Perm P,(p => q) = p' => q' )
assume ( p' = Perm P,p & q' = Perm P,q ) ; :: thesis: Perm P,(p => q) = p' => q'
hence Perm P,(p => q) = p' => q' by A1; :: thesis: verum