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 A: 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
B1: for w being Element of E ^omega st w ^ v = u holds
w1 = w and
B2: for w being Element of E ^omega st w ^ v = u holds
w2 = w ; :: thesis: w1 = w2
( w1 = w & w2 = w ) by A, B1, B2;
hence w1 = w2 ; :: 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