let P, Q, R be FinSequence-membered set ; :: thesis: (P ^ Q) ^ R = P ^ (Q ^ R)
for a being object holds
( a in (P ^ Q) ^ R iff a in P ^ (Q ^ R) )

proof

let a be object ; :: thesis: ( a in (P ^ Q) ^ R iff a in P ^ (Q ^ R) )
thus ( a in (P ^ Q) ^ R implies a in P ^ (Q ^ R) ) :: thesis: ( a in P ^ (Q ^ R) implies a in (P ^ Q) ^ R )

proof

assume a in (P ^ Q) ^ R ; :: thesis: a in P ^ (Q ^ R)
then consider u, r being FinSequence such that
A2: a = u ^ r and
A3: u in P ^ Q and
A4: r in R by Def2;
consider p, q being FinSequence such that
A5: u = p ^ q and
A6: p in P and
A7: q in Q by A3, Def2;
A8: a = p ^ (q ^ r) by A2, A5, FINSEQ_1:32;
q ^ r in Q ^ R by A4, A7, Def2;
hence a in P ^ (Q ^ R) by A6, A8, Def2; :: thesis: verum

end;

assume a in P ^ (Q ^ R) ; :: thesis: a in (P ^ Q) ^ R
then consider p, t being FinSequence such that
A9: a = p ^ t and
A10: p in P and
A11: t in Q ^ R by Def2;
consider q, r being FinSequence such that
A12: t = q ^ r and
A13: q in Q and
A14: r in R by A11, Def2;
A15: a = (p ^ q) ^ r by A9, A12, FINSEQ_1:32;
p ^ q in P ^ Q by A10, A13, Def2;
hence a in (P ^ Q) ^ R by A14, A15, Def2; :: thesis: verum

end;

hence (P ^ Q) ^ R = P ^ (Q ^ R) by TARSKI:2; :: thesis: verum