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]
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 ;
( 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] )
;
( S2[r '&' s] & S2[r => s] )
reconsider f =
Perm (
(v tohilbperm),
r) as
V67()
Permutation of
(SetVal ((v tohilbval),r)) by B1;
reconsider h =
Perm (
(v tohilbperm),
s) as
V67()
Permutation of
(SetVal ((v tohilbval),s)) by B1;
thus
S2[
r '&' s]
S2[r => s]
let F be
Function;
( F = (Perm (v tohilbperm)) . (r => s) implies F is involutive )
assume
F = (Perm (v tohilbperm)) . (r => s)
;
F is involutive
then F =
Perm (
(v tohilbperm),
(r => s))
.=
f => h
by HILBERT3:36
;
hence
F is
involutive
;
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
; verum