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 S2[ Element of HP-WFF ] means M1 . $1 = M2 . $1;
A8: for r, s being Element of HP-WFF st S2[r] & S2[s] holds
( S2[r '&' s] & S2[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S2[r] & S2[s] implies ( S2[r '&' s] & S2[r => s] ) )
assume A9: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S2[r '&' s] & S2[r => s] )
thus M1 . (r '&' s) = [:(M2 . r),(M2 . s):] by A4, A9
.= M2 . (r '&' s) by A7 ; :: thesis: S2[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 S2[ prop n]
proof
let n be Element of NAT ; :: thesis: S2[ prop n]
thus M1 . (prop n) = V . n by A3
.= M2 . (prop n) by A6 ; :: thesis: verum
end;
A11: S2[ VERUM ] by A2, A5;
for r being Element of HP-WFF holds S2[r] from HILBERT2:sch 2(A11, A10, A8);
 then for r being object st r in HP-WFF holds
M1 . r = M2 . r ;
hence M1 = M2 by PBOOLE:3; :: thesis: verum