let M1, M2 be ManySortedSet of HP-WFF ; :: thesis: ( 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)) ) ; :: thesis: M1 = M2

defpred S_{1}[ Element of HP-WFF ] means M1 . $1 = M2 . $1;

A8: for r, s being Element of HP-WFF st S_{1}[r] & S_{1}[s] holds

( S_{1}[r '&' s] & S_{1}[r => s] )
_{1}[ prop n]
_{1}[ VERUM ]
by A2, A5;

for r being Element of HP-WFF holds S_{1}[r]
from HILBERT2:sch 2(A11, A10, A8);

hence M1 = M2 ; :: thesis: verum

( 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)) ) ; :: thesis: M1 = M2

defpred S

A8: for r, s being Element of HP-WFF st S

( S

proof

A10:
for n being Element of NAT holds S
let r, s be Element of HP-WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r '&' s] & S_{1}[r => s] ) )

assume A9: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S_{1}[r '&' s] & S_{1}[r => s] )

thus M1 . (r '&' s) = [:(M2 . r),(M2 . s):] by A4, A9

.= M2 . (r '&' s) by A7 ; :: thesis: S_{1}[r => s]

thus M1 . (r => s) = Funcs ((M2 . r),(M2 . s)) by A4, A9

.= M2 . (r => s) by A7 ; :: thesis: verum

end;assume A9: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S

thus M1 . (r '&' s) = [:(M2 . r),(M2 . s):] by A4, A9

.= M2 . (r '&' s) by A7 ; :: thesis: S

thus M1 . (r => s) = Funcs ((M2 . r),(M2 . s)) by A4, A9

.= M2 . (r => s) by A7 ; :: thesis: verum

proof

A11:
S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

thus M1 . (prop n) = V . n by A3

.= M2 . (prop n) by A6 ; :: thesis: verum

end;thus M1 . (prop n) = V . n by A3

.= M2 . (prop n) by A6 ; :: thesis: verum

for r being Element of HP-WFF holds S

hence M1 = M2 ; :: thesis: verum