let R be non empty well-unital associative doubleLoopStr ; :: thesis: for a, b being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds
F ^ G is_a_factorization_of a * b
let a, b be Element of R; :: thesis: for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds
F ^ G is_a_factorization_of a * b
let F, G be non empty FinSequence of R; :: thesis: ( F is_a_factorization_of a & G is_a_factorization_of b implies F ^ G is_a_factorization_of a * b )
assume AS: ( F is_a_factorization_of a & G is_a_factorization_of b ) ; :: thesis: F ^ G is_a_factorization_of a * b
reconsider FG = F ^ G as non empty FinSequence of R ;
rng F c= the carrier of R ;
then reconsider f = F as Function of (dom F),R by FUNCT_2:2;
rng G c= the carrier of R ;
then reconsider g = G as Function of (dom G),R by FUNCT_2:2;
rng FG c= the carrier of R ;
then reconsider fg = FG as Function of (dom FG),R by FUNCT_2:2;

now :: thesis: for i being Element of dom (F ^ G) holds (F ^ G) . i is irreducible

let i be Element of dom (F ^ G); :: thesis: (F ^ G) . i is irreducible

now :: thesis: (F ^ G) . i is irreducible

per cases ( i in dom F or ex n being Nat st
( n in dom G & i = (len F) + n ) ) by FINSEQ_1:25;

suppose B: i in dom F ; :: thesis: (F ^ G) . i is irreducible

fg . i = f . i by B, FINSEQ_1:def 7;
hence (F ^ G) . i is irreducible by B, AS; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom G & i = (len F) + n ) ; :: thesis: (F ^ G) . i is irreducible

then consider n being Nat such that
B: ( n in dom G & i = (len F) + n ) ;
fg . i = g . n by B, FINSEQ_1:def 7;
hence (F ^ G) . i is irreducible by B, AS; :: thesis: verum

end;

end;

end;

hence (F ^ G) . i is irreducible ; :: thesis: verum

end;

hence F ^ G is_a_factorization_of a * b by AS, GROUP_4:5; :: thesis: verum