let E be set ; :: thesis: for a being Element of E ^omega st a ^ a = a holds
a = {}
let a be Element of E ^omega ; :: thesis: ( a ^ a = a implies a = {} )
assume a ^ a = a ; :: thesis: a = {}
then (len a) + (len a) = len a by AFINSQ_1:17;
hence a = {} ; :: thesis: verum