defpred S_{1}[ Element of HP-WFF ] means Perm (P,V) is bijective ;

A1: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r '&' s] & S_{1}[r => s] )

then A3: S_{1}[ VERUM ]
;

for p being Element of HP-WFF holds S_{1}[p]
from HILBERT2:sch 2(A3, A1, A2);

hence Perm (P,p) is bijective ; :: thesis: verum

A1: for n being Element of NAT holds S

proof

A2:
for r, s being Element of HP-WFF st S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

( SetVal (V,(prop n)) = V . n & Perm (P,(prop n)) = P . n ) by Def2, Def5;

hence S_{1}[ prop n]
by Def4; :: thesis: verum

end;( SetVal (V,(prop n)) = V . n & Perm (P,(prop n)) = P . n ) by Def2, Def5;

hence S

( S

proof

Perm (P,VERUM) = id (SetVal (V,VERUM))
by Th32;
let r, s be Element of HP-WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r '&' s] & S_{1}[r => s] ) )

assume Perm (P,r) is bijective ; :: thesis: ( not S_{1}[s] or ( S_{1}[r '&' s] & S_{1}[r => s] ) )

then reconsider r9 = Perm (P,r) as Permutation of (SetVal (V,r)) ;

assume Perm (P,s) is bijective ; :: thesis: ( S_{1}[r '&' s] & S_{1}[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: S_{1}[r => s]

( SetVal (V,(r => s)) = Funcs ((SetVal (V,r)),(SetVal (V,s))) & Perm (P,(r => s)) = r9 => s9 ) by Def2, Th35;

hence S_{1}[r => s]
; :: thesis: verum

end;assume Perm (P,r) is bijective ; :: thesis: ( not S

then reconsider r9 = Perm (P,r) as Permutation of (SetVal (V,r)) ;

assume Perm (P,s) is bijective ; :: thesis: ( 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: S

( SetVal (V,(r => s)) = Funcs ((SetVal (V,r)),(SetVal (V,s))) & Perm (P,(r => s)) = r9 => s9 ) by Def2, Th35;

hence S

then A3: S

for p being Element of HP-WFF holds S

hence Perm (P,p) is bijective ; :: thesis: verum