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

consider M being ManySortedSet of HP-WFF such that

A1: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = H_{1}(n) ) & ( for p, q being Element of HP-WFF holds

( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) from HILBERT2:sch 4();

take M ; :: thesis: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

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

thus ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) by A1; :: thesis: verum

consider M being ManySortedSet of HP-WFF such that

A1: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = H

( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) from HILBERT2:sch 4();

take M ; :: thesis: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

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

thus ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds

( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) by A1; :: thesis: verum