defpred S₁[ Element of HP-WFF ] means Perm P,V is bijective ;
A1: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
( SetVal V,(prop n) = V . n & Perm P,(prop n) = P . n ) by Def2, Def5;
hence S₁[ prop n] by Def4; :: thesis: verum

end;

A2: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] )

proof

let r, s be Element of HP-WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r '&' s] & S₁[r => s] ) )
assume Perm P,r is bijective ; :: thesis: ( not S₁[s] or ( S₁[r '&' s] & S₁[r => s] ) )
then reconsider r9 = Perm P,r as Permutation of (SetVal V,r) ;
assume Perm P,s is bijective ; :: thesis: ( S₁[r '&' s] & S₁[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, Th35;
hence Perm P,(r '&' s) is bijective by Th25; :: thesis: S₁[r => s]
( SetVal V,(r => s) = Funcs (SetVal V,r),(SetVal V,s) & Perm P,(r => s) = r9 => s9 ) by Def2, Th36;
hence S₁[r => s] ; :: thesis: verum

end;

Perm P,VERUM = id (SetVal V,VERUM ) by Th33;
then A3: S₁[ VERUM ] ;
for p being Element of HP-WFF holds S₁[p] from HILBERT2:sch 2(A3, A1, A2);
hence Perm P,p is bijective ; :: thesis: verum