let E be set ; :: thesis: for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C)
let A, B, C be Subset of (E ^omega); :: thesis: (A ^^ B) ^^ C = A ^^ (B ^^ C)
now :: thesis: for x being object holds
( ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) & ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C ) )
let x be object ; :: thesis: ( ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) & ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C ) )
thus ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) :: thesis: ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C )
proof
assume x in (A ^^ B) ^^ C ; :: thesis: x in A ^^ (B ^^ C)
then consider ab, c being Element of E ^omega such that
A1: ab in A ^^ B and
A2: ( c in C & x = ab ^ c ) by Def1;
consider a, b being Element of E ^omega such that
A3: a in A and
A4: ( b in B & ab = a ^ b ) by A1, Def1;
( x = a ^ (b ^ c) & b ^ c in B ^^ C ) by A2, A4, Def1, AFINSQ_1:27;
hence x in A ^^ (B ^^ C) by A3, Def1; :: thesis: verum
end;
assume x in A ^^ (B ^^ C) ; :: thesis: x in (A ^^ B) ^^ C
then consider a, bc being Element of E ^omega such that
A5: a in A and
A6: bc in B ^^ C and
A7: x = a ^ bc by Def1;
consider b, c being Element of E ^omega such that
A8: b in B and
A9: c in C and
A10: bc = b ^ c by A6, Def1;
( x = (a ^ b) ^ c & a ^ b in A ^^ B ) by A5, A7, A8, A10, Def1, AFINSQ_1:27;
hence x in (A ^^ B) ^^ C by A9, Def1; :: thesis: verum
end;
hence (A ^^ B) ^^ C = A ^^ (B ^^ C) by TARSKI:2; :: thesis: verum