let G be Group; :: thesis: for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
let a, b, c, d be Element of G; :: thesis: {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
thus {a,b} |^ {c,d} c= {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} :: according to XBOOLE_0:def 10 :: thesis: {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} c= {a,b} |^ {c,d}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b} |^ {c,d} or x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} )
assume x in {a,b} |^ {c,d} ; :: thesis: x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
then consider g, h being Element of G such that
A1: x = g |^ h and
A2: g in {a,b} and
A3: h in {c,d} ;
A4: ( h = c or h = d ) by A3, TARSKI:def 2;
( g = a or g = b ) by A2, TARSKI:def 2;
hence x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} by A1, A4, ENUMSET1:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} or x in {a,b} |^ {c,d} )
A5: ( c in {c,d} & d in {c,d} ) by TARSKI:def 2;
assume x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} ; :: thesis: x in {a,b} |^ {c,d}
then A6: ( x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d ) by ENUMSET1:def 2;
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
hence x in {a,b} |^ {c,d} by A6, A5; :: thesis: verum