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 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] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r '&' s] & S1[r => s] ) )
assume A9: ( M1 . r = M2 . r & M1 . s = M2 . s ) ; :: thesis: ( S1[r '&' s] & S1[r => s] )
thus M1 . (r '&' s) = [:(M2 . r),(M2 . s):] by A4, A9
.= M2 . (r '&' s) by A7 ; :: thesis: S1[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 S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
thus M1 . (prop n) = V . n by A3
.= M2 . (prop n) by A6 ; :: thesis: verum
end;
A11: S1[ VERUM ] by A2, A5;
for r being Element of HP-WFF holds S1[r] from hence M1 = M2 ; :: thesis: verum