let R be non empty doubleLoopStr ; :: thesis: for h, f, g being FinSequence of R holds
( h = f ^ g iff ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) ) )
let h, f, g be FinSequence of R; :: thesis: ( h = f ^ g iff ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) ) )
A1: len f >= 0 by NAT_1:2;
thus ( h = f ^ g implies ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) ) ) :: thesis: ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) implies h = f ^ g )

proof

assume A2: h = f ^ g ; :: thesis: ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) )
hence dom h = Seg ((len f) + (len g)) by FINSEQ_1:def 7; :: thesis: ( ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) )
then A3: len h = (len f) + (len g) by FINSEQ_1:def 3;
thus for k being Nat st k in dom f holds
h /. k = f /. k :: thesis: for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k

proof

let k be Nat; :: thesis: ( k in dom f implies h /. k = f /. k )
assume A4: k in dom f ; :: thesis: h /. k = f /. k
A5: len f <= (len f) + (len g) by NAT_1:11;
( 1 <= k & k <= len f ) by A4, FINSEQ_3:27;
then ( 1 <= k & k <= len h ) by A3, A5, XXREAL_0:2;
then k in dom h by FINSEQ_3:27;
then h /. k = h . k by PARTFUN1:def 8
.= f . k by A2, A4, FINSEQ_1:def 7
.= f /. k by A4, PARTFUN1:def 8 ;
hence h /. k = f /. k ; :: thesis: verum

end;

thus for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k :: thesis: verum

proof

let k be Nat; :: thesis: ( k in dom g implies h /. ((len f) + k) = g /. k )
assume A6: k in dom g ; :: thesis: h /. ((len f) + k) = g /. k
then A7: ( 1 <= k & k <= len g ) by FINSEQ_3:27;
then A8: 0 + 1 <= (len f) + k by A1, XREAL_1:9;
(len f) + k <= (len f) + (len g) by A7, XREAL_1:9;
then (len f) + k in dom h by A3, A8, FINSEQ_3:27;
then h /. ((len f) + k) = h . ((len f) + k) by PARTFUN1:def 8
.= g . k by A2, A6, FINSEQ_1:def 7
.= g /. k by A6, PARTFUN1:def 8 ;
hence h /. ((len f) + k) = g /. k ; :: thesis: verum

end;

end;

assume that
A9: dom h = Seg ((len f) + (len g)) and
A10: for k being Nat st k in dom f holds
h /. k = f /. k and
A11: for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ; :: thesis: h = f ^ g
A12: len h = (len f) + (len g) by A9, FINSEQ_1:def 3;
A13: for k being Nat st k in dom f holds
h . k = f . k

proof

let k be Nat; :: thesis: ( k in dom f implies h . k = f . k )
assume A14: k in dom f ; :: thesis: h . k = f . k
A15: len f <= (len f) + (len g) by NAT_1:11;
( 1 <= k & k <= len f ) by A14, FINSEQ_3:27;
then ( 1 <= k & k <= len h ) by A12, A15, XXREAL_0:2;
then k in dom h by FINSEQ_3:27;
then h . k = h /. k by PARTFUN1:def 8
.= f /. k by A10, A14
.= f . k by A14, PARTFUN1:def 8 ;
hence h . k = f . k ; :: thesis: verum

end;

for k being Nat st k in dom g holds
h . ((len f) + k) = g . k

proof

let k be Nat; :: thesis: ( k in dom g implies h . ((len f) + k) = g . k )
assume A16: k in dom g ; :: thesis: h . ((len f) + k) = g . k
then ( 1 <= k & k <= len g ) by FINSEQ_3:27;
then ( 0 + 1 <= (len f) + k & (len f) + k <= (len f) + (len g) ) by A1, XREAL_1:9;
then (len f) + k in dom h by A12, FINSEQ_3:27;
then h . ((len f) + k) = h /. ((len f) + k) by PARTFUN1:def 8
.= g /. k by A11, A16
.= g . k by A16, PARTFUN1:def 8 ;
hence h . ((len f) + k) = g . k ; :: thesis: verum

end;

hence h = f ^ g by A9, A13, FINSEQ_1:def 7; :: thesis: verum