deffunc H1( Element of NAT ) -> set = P . $1;
defpred S1[ 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 p' being Permutation of SetVal V,$1 ex q' being Permutation of SetVal V,$2 st
( p' = $3 & q' = $4 & $5 = p' => q' ) ) & ( ( not $3 is Permutation of SetVal V,$1 or not $4 is Permutation of SetVal V,$2 ) implies $5 = {} ) );
defpred S2[ 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 p' being Permutation of SetVal V,$1 ex q' being Permutation of SetVal V,$2 st
( p' = $3 & q' = $4 & $5 = [:p',q':] ) ) & ( ( 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 S2[p,q,a,b,c]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex c being set st S2[p,q,a,b,c]
let a, b be set ; :: thesis: ex c being set st S2[p,q,a,b,c]
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 ) ;
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 S2[p,q,a,b,c]
reconsider q' = b as Permutation of SetVal V,q by A3;
reconsider p' = a as Permutation of SetVal V,p by A2;
take [:p',q':] ; :: thesis: S2[p,q,a,b,[:p',q':]]
thus S2[p,q,a,b,[:p',q':]] ; :: thesis: verum
end;
suppose ( not a is Permutation of SetVal V,p or not b is Permutation of SetVal V,q ) ; :: thesis: ex c being set st S2[p,q,a,b,c]
hence ex c being set st S2[p,q,a,b,c] ; :: thesis: verum
end;
end;
end;
A4: for p, q being Element of HP-WFF
for a, b being set ex d being set st S1[p,q,a,b,d]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex d being set st S1[p,q,a,b,d]
let a, b be set ; :: thesis: ex d being set st S1[p,q,a,b,d]
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 ) ;
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 S1[p,q,a,b,d]
reconsider q' = b as Permutation of SetVal V,q by A6;
reconsider p' = a as Permutation of SetVal V,p by A5;
take p' => q' ; :: thesis: S1[p,q,a,b,p' => q']
thus S1[p,q,a,b,p' => q'] ; :: thesis: verum
end;
suppose ( not a is Permutation of SetVal V,p or not b is Permutation of SetVal V,q ) ; :: thesis: ex d being set st S1[p,q,a,b,d]
hence ex d being set st S1[p,q,a,b,d] ; :: thesis: verum
end;
end;
end;
A7: for p, q being Element of HP-WFF
for a, b, c, d being set st S1[p,q,a,b,c] & S1[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 S2[p,q,a,b,c] & S2[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) = H1(n) and
A11: for p, q being Element of HP-WFF holds
( S2[p,q,M . p,M . q,M . (p '&' q)] & S1[p,q,M . p,M . q,M . (p => q)] ) from HILBERT2:sch 3(A1, A4, A8, A7);
 defpred S3[ Element of HP-WFF ] means M . $1 is Permutation of (SetVal V) . $1;
A12: for r, s being Element of HP-WFF st S3[r] & S3[s] holds
( S3[r '&' s] & S3[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S3[r] & S3[s] implies ( S3[r '&' s] & S3[r => s] ) )
assume A13: ( M . r is Permutation of (SetVal V) . r & M . s is Permutation of (SetVal V) . s ) ; :: thesis: ( S3[r '&' s] & S3[r => s] )
A14: (SetVal V) . (r '&' s) = [:(SetVal V,r),(SetVal V,s):] by Def2;
ex p' being Permutation of SetVal V,r ex q' being Permutation of SetVal V,s st
( p' = M . r & q' = M . s & M . (r '&' s) = [:p',q':] ) by A11, A13;
hence M . (r '&' s) is Permutation of (SetVal V) . (r '&' s) by A14, Th25; :: thesis: S3[r => s]
A15: (SetVal V) . (r => s) = Funcs (SetVal V,r),(SetVal V,s) by Def2;
ex p' being Permutation of SetVal V,r ex q' being Permutation of SetVal V,s st
( p' = M . r & q' = M . s & M . (r => s) = p' => q' ) by A11, A13;
hence S3[r => s] by A15; :: thesis: verum
end;
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 p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' ) ) )
A16: for n being Element of NAT holds S3[ prop n]
proof
let n be Element of NAT ; :: thesis: S3[ prop n]
( M . (prop n) = P . n & (SetVal V) . (prop n) = V . n ) by A10, Def2;
hence S3[ prop n] by Def4; :: thesis: verum
end;
(SetVal V) . VERUM = 1 by Def2;
then A17: S3[ VERUM ] by A9;
A18: for p being Element of HP-WFF holds S3[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 p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' ) ) )
proof
let p be set ; :: according to PBOOLE:def 18 :: 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 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 p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' ) ) )
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 p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' )
let p, q be Element of HP-WFF ; :: thesis: ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' )
A19: ( M . p is Permutation of (SetVal V) . p & M . q is Permutation of (SetVal V) . q ) by A18;
then consider p' being Permutation of SetVal V,p, q' being Permutation of SetVal V,q such that
A20: ( p' = M . p & q' = M . q ) and
A21: M . (p '&' q) = [:p',q':] by A11;
take p' ; :: thesis: ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' )
take q' ; :: thesis: ( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] & M . (p => q) = p' => q' )
thus ( p' = M . p & q' = M . q & M . (p '&' q) = [:p',q':] ) by A20, A21; :: thesis: M . (p => q) = p' => q'
ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = M . p & q' = M . q & M . (p => q) = p' => q' ) by A11, A19;
hence M . (p => q) = p' => q' by A20; :: thesis: verum