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 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 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 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 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 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: S2[p,q,a,b,[:p9,q9:]]
thus S2[p,q,a,b,[:p9,q9:]] ; :: 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 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: S1[p,q,a,b,p9 => q9]
thus S1[p,q,a,b,p9 => q9] ; :: 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 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: S3[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 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 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 ) ) )
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 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
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 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
( 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