let s be non empty typealg ; :: thesis: for p being Proof of s
for v being Element of dom p st (p . v) `2 = 0 holds
ex x being type of s st (p . v) `1 = [<*x*>,x]
let p be Proof of s; :: thesis: for v being Element of dom p st (p . v) `2 = 0 holds
ex x being type of s st (p . v) `1 = [<*x*>,x]
let v be Element of dom p; :: thesis: ( (p . v) `2 = 0 implies ex x being type of s st (p . v) `1 = [<*x*>,x] )
v is correct by Def12;
hence ( (p . v) `2 = 0 implies ex x being type of s st (p . v) `1 = [<*x*>,x] ) by Def4; :: thesis: verum