defpred S1[ Element of HP-WFF ] means Perm (P,V) is bijective ;
A1: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
( SetVal (V,(prop n)) = V . n & Perm (P,(prop n)) = P . n ) by Def2, Def5;
hence S1[ prop n] by Def4; :: thesis: verum
end;
A2: for r, s being Element of HP-WFF st S1[r] & S1[s] holds
( S1[r '&' s] & S1[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r '&' s] & S1[r => s] ) )
assume Perm (P,r) is bijective ; :: thesis: ( not S1[s] or ( S1[r '&' s] & S1[r => s] ) )
then reconsider r9 = Perm (P,r) as Permutation of (SetVal (V,r)) ;
assume Perm (P,s) is bijective ; :: thesis: ( S1[r '&' s] & S1[r => s] )
then reconsider s9 = Perm (P,s) as Permutation of (SetVal (V,s)) ;
( SetVal (V,(r '&' s)) = [:(SetVal (V,r)),(SetVal (V,s)):] & Perm (P,(r '&' s)) = [:r9,s9:] ) by Def2, Th34;
hence Perm (P,(r '&' s)) is bijective ; :: thesis: S1[r => s]
( SetVal (V,(r => s)) = Funcs ((SetVal (V,r)),(SetVal (V,s))) & Perm (P,(r => s)) = r9 => s9 ) by Def2, Th35;
hence S1[r => s] ; :: thesis: verum
end;
Perm (P,VERUM) = id (SetVal (V,VERUM)) by Th32;
then A3: S1[ VERUM ] ;
for p being Element of HP-WFF holds S1[p] from HILBERT2:sch 2(A3, A1, A2);
 hence Perm (P,p) is bijective ; :: thesis: verum