let G be Group; for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)}
let a, b, c be Element of G; {a,b} |^ {c} = {(a |^ c),(b |^ c)}
thus
{a,b} |^ {c} c= {(a |^ c),(b |^ c)}
XBOOLE_0:def 10 {(a |^ c),(b |^ c)} c= {a,b} |^ {c}proof
let x be
object ;
TARSKI:def 3 ( not x in {a,b} |^ {c} or x in {(a |^ c),(b |^ c)} )
assume
x in {a,b} |^ {c}
;
x in {(a |^ c),(b |^ c)}
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}
;
A4:
(
g = b or
g = a )
by A2, TARSKI:def 2;
h = c
by A3, TARSKI:def 1;
hence
x in {(a |^ c),(b |^ c)}
by A1, A4, TARSKI:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {(a |^ c),(b |^ c)} or x in {a,b} |^ {c} )
A5:
c in {c}
by TARSKI:def 1;
assume
x in {(a |^ c),(b |^ c)}
; x in {a,b} |^ {c}
then A6:
( x = a |^ c or x = b |^ c )
by TARSKI:def 2;
( a in {a,b} & b in {a,b} )
by TARSKI:def 2;
hence
x in {a,b} |^ {c}
by A6, A5; verum