let G be Group; 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; {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)}
XBOOLE_0:def 10 {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} c= {a,b} |^ {c,d}proof
let x be
object ;
TARSKI:def 3 ( 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}
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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)}
; 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; verum