thus ( ex w being Element of E ^omega st w ^ v = u implies ex w1 being Element of E ^omega st
for w being Element of E ^omega st w ^ v = u holds
w1 = w ) :: thesis: ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b₁ being Element of E ^omega st b₁ = u )

proof

given w1 being Element of E ^omega such that A1: w1 ^ v = u ; :: thesis: ex w1 being Element of E ^omega st
for w being Element of E ^omega st w ^ v = u holds
w1 = w
take w1 ; :: thesis: for w being Element of E ^omega st w ^ v = u holds
w1 = w
let w be Element of E ^omega ; :: thesis: ( w ^ v = u implies w1 = w )
assume w ^ v = u ; :: thesis: w1 = w
hence w1 = w by A1, AFINSQ_1:28; :: thesis: verum

end;

thus ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b₁ being Element of E ^omega st b₁ = u ) ; :: thesis: verum