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

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 . O2end;

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