let M1, M2 be ManySortedSet of HP-WFF ; ( M1 . VERUM = 1 & ( for n being Element of NAT holds M1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( M1 . (p '&' q) = [:(M1 . p),(M1 . q):] & M1 . (p => q) = Funcs ((M1 . p),(M1 . q)) ) ) & M2 . VERUM = 1 & ( for n being Element of NAT holds M2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( M2 . (p '&' q) = [:(M2 . p),(M2 . q):] & M2 . (p => q) = Funcs ((M2 . p),(M2 . q)) ) ) implies M1 = M2 )
assume that
A2:
M1 . VERUM = 1
and
A3:
for n being Element of NAT holds M1 . (prop n) = V . n
and
A4:
for p, q being Element of HP-WFF holds
( M1 . (p '&' q) = [:(M1 . p),(M1 . q):] & M1 . (p => q) = Funcs ((M1 . p),(M1 . q)) )
and
A5:
M2 . VERUM = 1
and
A6:
for n being Element of NAT holds M2 . (prop n) = V . n
and
A7:
for p, q being Element of HP-WFF holds
( M2 . (p '&' q) = [:(M2 . p),(M2 . q):] & M2 . (p => q) = Funcs ((M2 . p),(M2 . q)) )
; M1 = M2
defpred S1[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A8:
for r, s being Element of HP-WFF st S1[r] & S1[s] holds
( S1[r '&' s] & S1[r => s] )
A10:
for n being Element of NAT holds S1[ prop n]
A11:
S1[ VERUM ]
by A2, A5;
for r being Element of HP-WFF holds S1[r]
from HILBERT2:sch 2(A11, A10, A8);
hence
M1 = M2
; verum