let pq be Sequence; :: thesis: ( pq = p ^ q iff ( dom pq = (len p) + (len q) & ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) ) )
A1: (len p) +^ (len q) = (len p) + (len q) by CARD_2:36;

hereby :: thesis: ( dom pq = (len p) + (len q) & ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) implies pq = p ^ q )

assume A2: pq = p ^ q ; :: thesis: ( dom pq = (len p) + (len q) & ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) )
hence dom pq = (len p) + (len q) by A1, ORDINAL4:def 1; :: thesis: ( ( for k being Nat st k in dom p holds
pq . k = p . k ) & ( for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ) )
thus for k being Nat st k in dom p holds
pq . k = p . k by A2, ORDINAL4:def 1; :: thesis: for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k
let k be Nat; :: thesis: ( k in dom q implies pq . ((len p) + k) = q . k )
assume k in dom q ; :: thesis: pq . ((len p) + k) = q . k
then ( pq . ((len p) +^ k) = q . k & k in NAT ) by A2, ORDINAL4:def 1;
hence pq . ((len p) + k) = q . k by CARD_2:36; :: thesis: verum

end;

assume that
A3: dom pq = (len p) + (len q) and
A4: for k being Nat st k in dom p holds
pq . k = p . k and
A5: for k being Nat st k in dom q holds
pq . ((len p) + k) = q . k ; :: thesis: pq = p ^ q

A6: now :: thesis: for a being Ordinal st a in dom q holds
pq . ((dom p) +^ a) = q . a

let a be Ordinal; :: thesis: ( a in dom q implies pq . ((dom p) +^ a) = q . a )
assume A7: a in dom q ; :: thesis: pq . ((dom p) +^ a) = q . a
then reconsider k = a as Element of NAT ;
thus pq . ((dom p) +^ a) = pq . ((len p) + k) by CARD_2:36
.= q . a by A5, A7 ; :: thesis: verum

end;

for a being Ordinal st a in dom p holds
pq . a = p . a by A4;
hence pq = p ^ q by A1, A3, A6, ORDINAL4:def 1; :: thesis: verum