set P = v tohilbperm ;
set V = v tohilbval ;
set fP = Perm (v tohilbperm);
defpred S2[ set ] means for f being Function st f = (Perm (v tohilbperm)) . p holds
f is involutive ;
A0: S2[ VERUM ] by HILBERT3:def 5;
A1: for n being Element of NAT holds S2[ prop n]
proof
let n be Element of NAT ; :: thesis: S2[ prop n]
let f be Function; :: thesis: ( f = (Perm (v tohilbperm)) . (prop n) implies f is involutive )
assume f = (Perm (v tohilbperm)) . (prop n) ; :: thesis: f is involutive
then f = (v tohilbperm) . n by HILBERT3:def 5
.= (v . n) tohilb by Lm34 ;
hence f is involutive ; :: thesis: verum
end;
A2: for r, s being Element of HP-WFF st S2[r] & S2[s] holds
( S2[r '&' s] & S2[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S2[r] & S2[s] implies ( S2[r '&' s] & S2[r => s] ) )
set a = r '&' s;
set i = r => s;
set f = Perm ((v tohilbperm),r);
set h = Perm ((v tohilbperm),s);
set F = SetVal ((v tohilbval),r);
set H = SetVal ((v tohilbval),s);
assume B1: ( S2[r] & S2[s] ) ; :: thesis: ( S2[r '&' s] & S2[r => s] )
reconsider f = Perm ((v tohilbperm),r) as involutive Permutation of (SetVal ((v tohilbval),r)) by B1;
reconsider h = Perm ((v tohilbperm),s) as involutive Permutation of (SetVal ((v tohilbval),s)) by B1;
thus S2[r '&' s] :: thesis: S2[r => s]
proof
let g be Function; :: thesis: ( g = (Perm (v tohilbperm)) . (r '&' s) implies g is involutive )
assume g = (Perm (v tohilbperm)) . (r '&' s) ; :: thesis: g is involutive
then g = Perm ((v tohilbperm),(r '&' s))
.= [:f,h:] by HILBERT3:35 ;
hence g is involutive ; :: thesis: verum
end;
let F be Function; :: thesis: ( F = (Perm (v tohilbperm)) . (r => s) implies F is involutive )
assume F = (Perm (v tohilbperm)) . (r => s) ; :: thesis: F is involutive
then F = Perm ((v tohilbperm),(r => s))
.= f => h by HILBERT3:36 ;
hence F is involutive ; :: thesis: verum
end;
for p being Element of HP-WFF holds S2[p] from HILBERT2:sch 2(A0, A1, A2);
 hence Perm ((v tohilbperm),p) is involutive ; :: thesis: verum