let p, q, r be FinSequence; :: thesis: (p ^ q) ^ r = p ^ (q ^ r)
A1: dom ((p ^ q) ^ r) = Seg ((len (p ^ q)) + (len r)) by Def7
.= Seg (((len p) + (len q)) + (len r)) by Th22
.= Seg ((len p) + ((len q) + (len r)))
.= Seg ((len p) + (len (q ^ r))) by Th22 ;
A2: 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 A3: k in dom p ; :: thesis: ((p ^ q) ^ r) . k = p . k
dom p c= dom (p ^ q) by Th26;
hence ((p ^ q) ^ r) . k = (p ^ q) . k by A3, Def7
.= p . k by A3, Def7 ;
:: thesis: verum

end;

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: ( k in dom q implies ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k )

assume A6: k in dom q ; :: thesis: ((p ^ q) ^ r) . ((len p) + k) = (q ^ r) . k
then (len p) + k in dom (p ^ q) by Th28;
hence ((p ^ q) ^ r) . ((len p) + k) = (p ^ q) . ((len p) + k) by Def7
.= q . k by A6, Def7
.= (q ^ r) . k by A6, Def7 ;
:: thesis: verum

end;

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
A7: n in dom r and
A8: k = (len q) + n by A4, Th25;
thus ((p ^ q) ^ r) . ((len p) + k) = ((p ^ q) ^ r) . (((len p) + (len q)) + n) by A8
.= ((p ^ q) ^ r) . ((len (p ^ q)) + n) by Th22
.= r . n by A7, Def7
.= (q ^ r) . k by A7, A8, Def7 ; :: thesis: verum

end;

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

end;

hence (p ^ q) ^ r = p ^ (q ^ r) by A1, A2, Def7; :: thesis: verum