let X be set ; :: thesis: for O1, O2 being Operation of X st ( for L being List of X holds L | O1 = L | O2 ) holds
O1 = O2
let O1, O2 be Operation of X; :: thesis: ( ( for L being List of X holds L | O1 = L | O2 ) implies O1 = O2 )
assume A1: for L being List of X holds L | O1 = L | O2 ; :: thesis: O1 = O2
now :: thesis: for x being Element of X holds x . O1 = x . O2
let x be Element of X; :: thesis: b1 . O1 = b1 . O2
per cases ( X <> {} or X = {} ) ;
suppose X <> {} ; :: thesis: b1 . O1 = b1 . O2
then reconsider L = {x} as Subset of X by ZFMISC_1:31;
thus x . O1 = L | O1
.= x . O2 by A1 ; :: thesis: verum
end;
suppose X = {} ; :: thesis: b1 . O1 = b1 . O2
hence x . O1 = x . O2 ; :: thesis: verum
end;
end;
end;
hence O1 = O2 by Th29; :: thesis: verum