let w1, w2 be Element of E ^omega ; :: thesis: ( ( ex w being Element of E ^omega st w ^ v = u & ( for w being Element of E ^omega st w ^ v = u holds
w1 = w ) & ( for w being Element of E ^omega st w ^ v = u holds
w2 = w ) implies w1 = w2 ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) & w1 = u & w2 = u implies w1 = w2 ) )

hereby :: thesis: ( ( for w being Element of E ^omega holds not w ^ v = u ) & w1 = u & w2 = u implies w1 = w2 )

given w being Element of E ^omega such that A2: w ^ v = u ; :: thesis: ( ( for w being Element of E ^omega st w ^ v = u holds
w1 = w ) & ( for w being Element of E ^omega st w ^ v = u holds
w2 = w ) implies w1 = w2 )
assume that
A3: for w being Element of E ^omega st w ^ v = u holds
w1 = w and
A4: for w being Element of E ^omega st w ^ v = u holds
w2 = w ; :: thesis: w1 = w2
w1 = w by A2, A3;
hence w1 = w2 by A2, A4; :: thesis: verum

end;

thus ( ( for w being Element of E ^omega holds not w ^ v = u ) & w1 = u & w2 = u implies w1 = w2 ) ; :: thesis: verum