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: b₁ . O1 = b₁ . O2

per cases ( X <> {} or X = {} ) ;

suppose X <> {} ; :: thesis: b₁ . O1 = b₁ . 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: b₁ . O1 = b₁ . O2

hence x . O1 = x . O2 ; :: thesis: verum

end;

end;

end;

hence O1 = O2 by Th29; :: thesis: verum