begin
theorem
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
for
a,
b,
x,
y,
x9,
y9 being
set st
a <> b &
a,
b --> x,
y = a,
b --> x9,
y9 holds
(
x = x9 &
y = y9 )
theorem Th11:
theorem Th12:
theorem Th13:
for
a,
b,
c,
d being
set st
a <> b holds
(a,b --> c,d) * (a,b --> b,a) = a,
b --> d,
c
theorem Th14:
begin
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem
canceled;
theorem Th23:
theorem Th24:
begin
theorem Th25:
definition
let A,
B be non
empty set ;
let P be
Permutation of
A;
let Q be
Function of
B,
B;
func P => Q -> Function of
(Funcs A,B),
(Funcs A,B) means :
Def1:
for
f being
Function of
A,
B holds
it . f = (Q * f) * (P " );
existence
ex b1 being Function of (Funcs A,B),(Funcs A,B) st
for f being Function of A,B holds b1 . f = (Q * f) * (P " )
uniqueness
for b1, b2 being Function of (Funcs A,B),(Funcs A,B) st ( for f being Function of A,B holds b1 . f = (Q * f) * (P " ) ) & ( for f being Function of A,B holds b2 . f = (Q * f) * (P " ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines => HILBERT3:def 1 :
theorem Th26:
theorem Th27:
theorem Th28:
begin
definition
let V be
SetValuation;
func SetVal V -> ManySortedSet of
HP-WFF means :
Def2:
(
it . VERUM = 1 & ( for
n being
Element of
NAT holds
it . (prop n) = V . n ) & ( for
p,
q being
Element of
HP-WFF holds
(
it . (p '&' q) = [:(it . p),(it . q):] &
it . (p => q) = Funcs (it . p),
(it . q) ) ) );
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs (b1 . p),(b1 . q) ) ) )
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs (b1 . p),(b1 . q) ) ) & b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs (b2 . p),(b2 . q) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines SetVal HILBERT3:def 2 :
:: deftheorem defines SetVal HILBERT3:def 3 :
theorem
theorem
theorem
theorem
registration
let V be
SetValuation;
let p,
q,
r be
Element of
HP-WFF ;
cluster Function-yielding Element of
bool [:(SetVal V,(p => q)),(SetVal V,(p => r)):];
existence
ex b1 being Function of (SetVal V,(p => q)),(SetVal V,(p => r)) st b1 is Function-yielding
cluster Function-yielding Element of
SetVal V,
(p => (q => r));
existence
ex b1 being Element of SetVal V,(p => (q => r)) st b1 is Function-yielding
end;
begin
:: deftheorem Def4 defines Permutation HILBERT3:def 4 :
definition
let V be
SetValuation;
let P be
Permutation of
V;
func Perm P -> ManySortedFunction of
SetVal V,
SetVal V means :
Def5:
(
it . VERUM = id 1 & ( for
n being
Element of
NAT holds
it . (prop n) = P . n ) & ( for
p,
q being
Element of
HP-WFF ex
p9 being
Permutation of
(SetVal V,p) ex
q9 being
Permutation of
(SetVal V,q) st
(
p9 = it . p &
q9 = it . q &
it . (p '&' q) = [:p9,q9:] &
it . (p => q) = p9 => q9 ) ) );
existence
ex b1 being ManySortedFunction of SetVal V, SetVal V st
( b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal V,p) ex q9 being Permutation of (SetVal V,q) st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = [:p9,q9:] & b1 . (p => q) = p9 => q9 ) ) )
uniqueness
for b1, b2 being ManySortedFunction of SetVal V, SetVal V st b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal V,p) ex q9 being Permutation of (SetVal V,q) st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = [:p9,q9:] & b1 . (p => q) = p9 => q9 ) ) & b2 . VERUM = id 1 & ( for n being Element of NAT holds b2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal V,p) ex q9 being Permutation of (SetVal V,q) st
( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = [:p9,q9:] & b2 . (p => q) = p9 => q9 ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines Perm HILBERT3:def 5 :
:: deftheorem defines Perm HILBERT3:def 6 :
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
begin
:: deftheorem Def7 defines canonical HILBERT3:def 7 :
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
begin
:: deftheorem Def8 defines pseudo-canonical HILBERT3:def 8 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th54:
theorem