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₁[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A8: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] )

proof

let r, s be Element of HP-WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r '&' s] & S₁[r => s] ) )
assume A9: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S₁[r '&' s] & S₁[r => s] )
thus M1 . (r '&' s) = [:(M2 . r),(M2 . s):] by A4, A9
.= M2 . (r '&' s) by A7 ; :: thesis: S₁[r => s]
thus M1 . (r => s) = Funcs ((M2 . r),(M2 . s)) by A4, A9
.= M2 . (r => s) by A7 ; :: thesis: verum

end;

A10: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
thus M1 . (prop n) = V . n by A3
.= M2 . (prop n) by A6 ; :: thesis: verum

end;

A11: S₁[ VERUM ] by A2, A5;
for r being Element of HP-WFF holds S₁[r] from HILBERT2:sch 2(A11, A10, A8);
hence M1 = M2 ; :: thesis: verum