defpred S1[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means $5 = F4($3,$4);
defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means $5 = F3($3,$4);
A1: for p, q being Element of HP-WFF
for a, b being set ex d being set st S1[p,q,a,b,d] ;
A2: 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 ;
A3: 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 ;
A4: for p, q being Element of HP-WFF
for a, b being set ex c being set st S2[p,q,a,b,c] ;
consider M being ManySortedSet of HP-WFF such that
A5: M . VERUM = F1() and
A6: for n being Element of NAT holds M . (prop n) = F2(n) and
A7: 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(A4, A1, A2, A3);
 take M ; :: thesis: ( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )
thus M . VERUM = F1() by A5; :: thesis: ( ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )
thus for n being Element of NAT holds M . (prop n) = F2(n) by A6; :: thesis: for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) )
let p, q be Element of HP-WFF ; :: thesis: ( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) )
set x = M . p;
set y = M . q;
thus M . (p '&' q) = F3((M . p),(M . q)) by A7; :: thesis: M . (p => q) = F4((M . p),(M . q))
thus M . (p => q) = F4((M . p),(M . q)) by A7; :: thesis: verum