let s be non empty typealg ; :: thesis: for p being Proof of s
for v being Element of dom p holds
not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7
let p be Proof of s; :: thesis: for v being Element of dom p holds
not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7
let v be Element of dom p; :: thesis: not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7
v is correct by Def12;
hence not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7 by Def4; :: thesis: verum