scheme :: HILBERT2:sch 3
HPMSSExL{ F1() -> set , F2( Element of NAT ) -> set , P1[ Element of HP-WFF , Element of HP-WFF , set , set , set ], P2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) )
provided
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st P1[p,q,a,b,c] and
A2: for p, q being Element of HP-WFF
for a, b being set ex d being set st P2[p,q,a,b,d] and
A3: for p, q being Element of HP-WFF
for a, b, c, d being set st P1[p,q,a,b,c] & P1[p,q,a,b,d] holds
c = d and
A4: for p, q being Element of HP-WFF
for a, b, c, d being set st P2[p,q,a,b,c] & P2[p,q,a,b,d] holds
c = d