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