let R be non empty doubleLoopStr ; :: thesis: for f, g, h 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 f, g, h 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
( len f <= (len f) + (len g) & k <= len f ) by A4, FINSEQ_3:25, NAT_1:11;
then A5: k <= len h by A3, XXREAL_0:2;
1 <= k by A4, FINSEQ_3:25;
then k in dom h by A5, FINSEQ_3:25;
then h /. k = h . k by PARTFUN1:def 6
.= f . k by A2, A4, FINSEQ_1:def 7
.= f /. k by A4, PARTFUN1:def 6 ;
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 k <= len g by FINSEQ_3:25;
then A7: (len f) + k <= (len f) + (len g) by XREAL_1:7;
1 <= k by A6, FINSEQ_3:25;
then 0 + 1 <= (len f) + k by A1, XREAL_1:7;
then (len f) + k in dom h by A3, A7, FINSEQ_3:25;
then h /. ((len f) + k) = h . ((len f) + k) by PARTFUN1:def 6
.= g . k by A2, A6, FINSEQ_1:def 7
.= g /. k by A6, PARTFUN1:def 6 ;
hence h /. ((len f) + k) = g /. k ; :: thesis: verum

end;

end;

assume that
A8: dom h = Seg ((len f) + (len g)) and
A9: for k being Nat st k in dom f holds
h /. k = f /. k and
A10: for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ; :: thesis: h = f ^ g
A11: len h = (len f) + (len g) by A8, FINSEQ_1:def 3;
A12: 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 A13: k in dom g ; :: thesis: h . ((len f) + k) = g . k
then k <= len g by FINSEQ_3:25;
then A14: (len f) + k <= (len f) + (len g) by XREAL_1:7;
1 <= k by A13, FINSEQ_3:25;
then 0 + 1 <= (len f) + k by A1, XREAL_1:7;
then (len f) + k in dom h by A11, A14, FINSEQ_3:25;
then h . ((len f) + k) = h /. ((len f) + k) by PARTFUN1:def 6
.= g /. k by A10, A13
.= g . k by A13, PARTFUN1:def 6 ;
hence h . ((len f) + k) = g . k ; :: thesis: verum

end;

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 A15: k in dom f ; :: thesis: h . k = f . k
( len f <= (len f) + (len g) & k <= len f ) by A15, FINSEQ_3:25, NAT_1:11;
then A16: k <= len h by A11, XXREAL_0:2;
1 <= k by A15, FINSEQ_3:25;
then k in dom h by A16, FINSEQ_3:25;
then h . k = h /. k by PARTFUN1:def 6
.= f /. k by A9, A15
.= f . k by A15, PARTFUN1:def 6 ;
hence h . k = f . k ; :: thesis: verum

end;

hence h = f ^ g by A8, A12, FINSEQ_1:def 7; :: thesis: verum