let f1, f2 be CompositionSeries of G; :: thesis: ( ( for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f1 . k = (1). G ) & len f1 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) & ( for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f2 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f2 . k = (1). G ) & len f2 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) implies f1 = f2 )
assume A90: for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f1 . k = (1). G ) & len f1 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ; :: thesis: ( ex k, i, j being Nat ex H1, H2, H3 being StableSubgroup of G st
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f2 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f2 . k = (1). G ) implies not len f2 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) or f1 = f2 )
assume A91: for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f2 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f2 . k = (1). G ) & len f2 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ; :: thesis: f1 = f2
then A92: dom f1 = Seg (len f2) by A90, FINSEQ_1:def 3
.= dom f2 by FINSEQ_1:def 3 ;

now

let k be Nat; :: thesis: ( k in dom f1 implies f1 . b₁ = f2 . b₁ )
assume A93: k in dom f1 ; :: thesis: f1 . b₁ = f2 . b₁
set l = len f1;
A94: k in Seg (len f1) by A93, FINSEQ_1:def 3;

per cases ( ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) or k = (((len s1) - 1) * ((len s2) - 1)) + 1 ) by A1, A90, A94, Lm45;

suppose ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ; :: thesis: f1 . b₁ = f2 . b₁

then consider i, j being Nat such that
A95: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ;
reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A95, Th111;
( f1 . k = H1 "\/" (H2 /\ H3) & f2 . k = H1 "\/" (H2 /\ H3) ) by A90, A91, A95;
hence f1 . k = f2 . k ; :: thesis: verum

end;

suppose k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: f1 . b₁ = f2 . b₁

then ( f1 . k = (1). G & f2 . k = (1). G ) by A90, A91;
hence f1 . k = f2 . k ; :: thesis: verum

end;

end;

end;

hence f1 = f2 by A92, FINSEQ_1:17; :: thesis: verum