let p, q, r be XFinSequence; :: thesis: (p ^ q) ^ r = p ^ (q ^ r)
A1: for k being Nat st k in dom p holds
((p ^ q) ^ r) . k = p . k

proof

let k be Nat; :: thesis: ( k in dom p implies ((p ^ q) ^ r) . k = p . k )
assume A2: k in dom p ; :: thesis: ((p ^ q) ^ r) . k = p . k
dom p c= dom (p ^ q) by Th19;
hence ((p ^ q) ^ r) . k = (p ^ q) . k by A2, Def3
.= p . k by A2, Def3 ;
:: thesis: verum

end;

A3: for k being Nat st k in dom (q ^ r) holds
((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k

proof

let k be Nat; :: thesis: ( k in dom (q ^ r) implies ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k )
assume A4: k in dom (q ^ r) ; :: thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k

A5: now :: thesis: ( not k in dom q implies ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k )

assume not k in dom q ; :: thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then consider n being Nat such that
A6: n in dom r and
A7: k = (len q) + n by A4, Th18;
thus ((p ^ q) ^ r) . ((len p) + k) = ((p ^ q) ^ r) . (((len p) + (len q)) + n) by A7
.= ((p ^ q) ^ r) . ((len (p ^ q)) + n) by Def3
.= r . n by A6, Def3
.= (q ^ r) . k by A6, A7, Def3 ; :: thesis: verum

end;

now :: thesis: ( k in dom q implies ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k )

assume A8: k in dom q ; :: thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then (len p) + k in dom (p ^ q) by Th21;
hence ((p ^ q) ^ r) . ((len p) + k) = (p ^ q) . ((len p) + k) by Def3
.= q . k by A8, Def3
.= (q ^ r) . k by A8, Def3 ;
:: thesis: verum

end;

hence ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k by A5; :: thesis: verum

end;

dom ((p ^ q) ^ r) = (len (p ^ q)) + (len r) by Def3
.= ((len p) + (len q)) + (len r) by Def3
.= (len p) + ((len q) + (len r))
.= (len p) + (len (q ^ r)) by Def3 ;
hence (p ^ q) ^ r = p ^ (q ^ r) by A1, A3, Def3; :: thesis: verum