deffunc H_{1}( Element of NAT ) -> set = P . $1;

defpred S_{1}[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is Permutation of (SetVal (V,$1)) & $4 is Permutation of (SetVal (V,$2)) implies ex p9 being Permutation of (SetVal (V,$1)) ex q9 being Permutation of (SetVal (V,$2)) st

( p9 = $3 & q9 = $4 & $5 = p9 => q9 ) ) & ( ( not $3 is Permutation of (SetVal (V,$1)) or not $4 is Permutation of (SetVal (V,$2)) ) implies $5 = {} ) );

defpred S_{2}[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is Permutation of (SetVal (V,$1)) & $4 is Permutation of (SetVal (V,$2)) implies ex p9 being Permutation of (SetVal (V,$1)) ex q9 being Permutation of (SetVal (V,$2)) st

( p9 = $3 & q9 = $4 & $5 = [:p9,q9:] ) ) & ( ( not $3 is Permutation of (SetVal (V,$1)) or not $4 is Permutation of (SetVal (V,$2)) ) implies $5 = {} ) );

A1: for p, q being Element of HP-WFF

for a, b being set ex c being set st S_{2}[p,q,a,b,c]

for a, b being set ex d being set st S_{1}[p,q,a,b,d]

for a, b, c, d being set st S_{1}[p,q,a,b,c] & S_{1}[p,q,a,b,d] holds

c = d ;

A8: for p, q being Element of HP-WFF

for a, b, c, d being set st S_{2}[p,q,a,b,c] & S_{2}[p,q,a,b,d] holds

c = d ;

consider M being ManySortedSet of HP-WFF such that

A9: M . VERUM = id 1 and

A10: for n being Element of NAT holds M . (prop n) = H_{1}(n)
and

A11: for p, q being Element of HP-WFF holds

( S_{2}[p,q,M . p,M . q,M . (p '&' q)] & S_{1}[p,q,M . p,M . q,M . (p => q)] )
from HILBERT2:sch 3(A1, A4, A8, A7);

defpred S_{3}[ Element of HP-WFF ] means M . $1 is Permutation of ((SetVal V) . $1);

A12: for r, s being Element of HP-WFF st S_{3}[r] & S_{3}[s] holds

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

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) )

A16: for n being Element of NAT holds S_{3}[ prop n]

then A17: S_{3}[ VERUM ]
by A9;

A18: for p being Element of HP-WFF holds S_{3}[p]
from HILBERT2:sch 2(A17, A16, A12);

thus M is ManySortedFunction of SetVal V, SetVal V :: thesis: ( M . VERUM = id 1 & ( for n being Element of NAT holds M . (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 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) )

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) )

thus for n being Element of NAT holds M . (prop n) = P . n by A10; :: thesis: 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 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

let p, q be Element of HP-WFF ; :: thesis: ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

A19: ( M . p is Permutation of ((SetVal V) . p) & M . q is Permutation of ((SetVal V) . q) ) by A18;

then consider p9 being Permutation of (SetVal (V,p)), q9 being Permutation of (SetVal (V,q)) such that

A20: ( p9 = M . p & q9 = M . q ) and

A21: M . (p '&' q) = [:p9,q9:] by A11;

take p9 ; :: thesis: ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

take q9 ; :: thesis: ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

thus ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] ) by A20, A21; :: thesis: M . (p => q) = p9 => q9

ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M . p & q9 = M . q & M . (p => q) = p9 => q9 ) by A11, A19;

hence M . (p => q) = p9 => q9 by A20; :: thesis: verum

defpred S

( p9 = $3 & q9 = $4 & $5 = p9 => q9 ) ) & ( ( not $3 is Permutation of (SetVal (V,$1)) or not $4 is Permutation of (SetVal (V,$2)) ) implies $5 = {} ) );

defpred S

( p9 = $3 & q9 = $4 & $5 = [:p9,q9:] ) ) & ( ( not $3 is Permutation of (SetVal (V,$1)) or not $4 is Permutation of (SetVal (V,$2)) ) implies $5 = {} ) );

A1: for p, q being Element of HP-WFF

for a, b being set ex c being set st S

proof

A4:
for p, q being Element of HP-WFF
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex c being set st S_{2}[p,q,a,b,c]

let a, b be set ; :: thesis: ex c being set st S_{2}[p,q,a,b,c]

end;let a, b be set ; :: thesis: ex c being set st S

per cases
( ( a is Permutation of (SetVal (V,p)) & b is Permutation of (SetVal (V,q)) ) or not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) )
;

end;

suppose that A2:
a is Permutation of (SetVal (V,p))
and

A3: b is Permutation of (SetVal (V,q)) ; :: thesis: ex c being set st S_{2}[p,q,a,b,c]

A3: b is Permutation of (SetVal (V,q)) ; :: thesis: ex c being set st S

reconsider q9 = b as Permutation of (SetVal (V,q)) by A3;

reconsider p9 = a as Permutation of (SetVal (V,p)) by A2;

take [:p9,q9:] ; :: thesis: S_{2}[p,q,a,b,[:p9,q9:]]

thus S_{2}[p,q,a,b,[:p9,q9:]]
; :: thesis: verum

end;reconsider p9 = a as Permutation of (SetVal (V,p)) by A2;

take [:p9,q9:] ; :: thesis: S

thus S

suppose
( not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) )
; :: thesis: ex c being set st S_{2}[p,q,a,b,c]

end;

end;

for a, b being set ex d being set st S

proof

A7:
for p, q being Element of HP-WFF
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex d being set st S_{1}[p,q,a,b,d]

let a, b be set ; :: thesis: ex d being set st S_{1}[p,q,a,b,d]

end;let a, b be set ; :: thesis: ex d being set st S

per cases
( ( a is Permutation of (SetVal (V,p)) & b is Permutation of (SetVal (V,q)) ) or not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) )
;

end;

suppose that A5:
a is Permutation of (SetVal (V,p))
and

A6: b is Permutation of (SetVal (V,q)) ; :: thesis: ex d being set st S_{1}[p,q,a,b,d]

A6: b is Permutation of (SetVal (V,q)) ; :: thesis: ex d being set st S

reconsider q9 = b as Permutation of (SetVal (V,q)) by A6;

reconsider p9 = a as Permutation of (SetVal (V,p)) by A5;

take p9 => q9 ; :: thesis: S_{1}[p,q,a,b,p9 => q9]

thus S_{1}[p,q,a,b,p9 => q9]
; :: thesis: verum

end;reconsider p9 = a as Permutation of (SetVal (V,p)) by A5;

take p9 => q9 ; :: thesis: S

thus S

suppose
( not a is Permutation of (SetVal (V,p)) or not b is Permutation of (SetVal (V,q)) )
; :: thesis: ex d being set st S_{1}[p,q,a,b,d]

end;

end;

for a, b, c, d being set st S

c = d ;

A8: for p, q being Element of HP-WFF

for a, b, c, d being set st S

c = d ;

consider M being ManySortedSet of HP-WFF such that

A9: M . VERUM = id 1 and

A10: for n being Element of NAT holds M . (prop n) = H

A11: for p, q being Element of HP-WFF holds

( S

defpred S

A12: for r, s being Element of HP-WFF st S

( S

proof

take
M
; :: thesis: ( M is ManySortedFunction of SetVal V, SetVal V & M . VERUM = id 1 & ( for n being Element of NAT holds M . (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
let r, s be Element of HP-WFF ; :: thesis: ( S_{3}[r] & S_{3}[s] implies ( S_{3}[r '&' s] & S_{3}[r => s] ) )

assume A13: ( M . r is Permutation of ((SetVal V) . r) & M . s is Permutation of ((SetVal V) . s) ) ; :: thesis: ( S_{3}[r '&' s] & S_{3}[r => s] )

A14: (SetVal V) . (r '&' s) = [:(SetVal (V,r)),(SetVal (V,s)):] by Def2;

ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M . r & q9 = M . s & M . (r '&' s) = [:p9,q9:] ) by A11, A13;

hence M . (r '&' s) is Permutation of ((SetVal V) . (r '&' s)) by A14; :: thesis: S_{3}[r => s]

A15: (SetVal V) . (r => s) = Funcs ((SetVal (V,r)),(SetVal (V,s))) by Def2;

ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M . r & q9 = M . s & M . (r => s) = p9 => q9 ) by A11, A13;

hence S_{3}[r => s]
by A15; :: thesis: verum

end;assume A13: ( M . r is Permutation of ((SetVal V) . r) & M . s is Permutation of ((SetVal V) . s) ) ; :: thesis: ( S

A14: (SetVal V) . (r '&' s) = [:(SetVal (V,r)),(SetVal (V,s)):] by Def2;

ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M . r & q9 = M . s & M . (r '&' s) = [:p9,q9:] ) by A11, A13;

hence M . (r '&' s) is Permutation of ((SetVal V) . (r '&' s)) by A14; :: thesis: S

A15: (SetVal V) . (r => s) = Funcs ((SetVal (V,r)),(SetVal (V,s))) by Def2;

ex p9 being Permutation of (SetVal (V,r)) ex q9 being Permutation of (SetVal (V,s)) st

( p9 = M . r & q9 = M . s & M . (r => s) = p9 => q9 ) by A11, A13;

hence S

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) )

A16: for n being Element of NAT holds S

proof

(SetVal V) . VERUM = 1
by Def2;
let n be Element of NAT ; :: thesis: S_{3}[ prop n]

( M . (prop n) = P . n & (SetVal V) . (prop n) = V . n ) by A10, Def2;

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

end;( M . (prop n) = P . n & (SetVal V) . (prop n) = V . n ) by A10, Def2;

hence S

then A17: S

A18: for p being Element of HP-WFF holds S

thus M is ManySortedFunction of SetVal V, SetVal V :: thesis: ( M . VERUM = id 1 & ( for n being Element of NAT holds M . (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 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) )

proof

thus
M . VERUM = id 1
by A9; :: thesis: ( ( for n being Element of NAT holds M . (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
let p be object ; :: according to PBOOLE:def 15 :: thesis: ( not p in HP-WFF or M . p is Element of bool [:((SetVal V) . p),((SetVal V) . p):] )

thus ( not p in HP-WFF or M . p is Element of bool [:((SetVal V) . p),((SetVal V) . p):] ) by A18; :: thesis: verum

end;thus ( not p in HP-WFF or M . p is Element of bool [:((SetVal V) . p),((SetVal V) . p):] ) by A18; :: thesis: verum

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 ) ) )

thus for n being Element of NAT holds M . (prop n) = P . n by A10; :: thesis: 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 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

let p, q be Element of HP-WFF ; :: thesis: ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

A19: ( M . p is Permutation of ((SetVal V) . p) & M . q is Permutation of ((SetVal V) . q) ) by A18;

then consider p9 being Permutation of (SetVal (V,p)), q9 being Permutation of (SetVal (V,q)) such that

A20: ( p9 = M . p & q9 = M . q ) and

A21: M . (p '&' q) = [:p9,q9:] by A11;

take p9 ; :: thesis: ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

take q9 ; :: thesis: ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] & M . (p => q) = p9 => q9 )

thus ( p9 = M . p & q9 = M . q & M . (p '&' q) = [:p9,q9:] ) by A20, A21; :: thesis: M . (p => q) = p9 => q9

ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st

( p9 = M . p & q9 = M . q & M . (p => q) = p9 => q9 ) by A11, A19;

hence M . (p => q) = p9 => q9 by A20; :: thesis: verum