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 A104: 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 A105: 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
A106: now :: thesis: for k being Nat st k in dom f1 holds
f1 . k = f2 . k
set l = len f1;
let k be Nat; :: thesis: ( k in dom f1 implies f1 . b1 = f2 . b1 )
assume k in dom f1 ; :: thesis: f1 . b1 = f2 . b1
then A107: k in Seg (len f1) by 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, A2, A104, A107, Lm44;
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 . b1 = f2 . b1
then consider i, j being Nat such that
A108: k = ((i - 1) * ((len s2) - 1)) + j and
A109: ( 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 A109, Th111;
f1 . k = H1 "\/" (H2 /\ H3) by A104, A108, A109;
hence f1 . k = f2 . k by A105, A108, A109; :: thesis: verum
end;
suppose A110: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: f1 . b1 = f2 . b1
then f1 . k = (1). G by A104;
hence f1 . k = f2 . k by A105, A110; :: thesis: verum
end;
end;
end;
dom f1 = Seg (len f2) by A104, A105, FINSEQ_1:def 3
.= dom f2 by FINSEQ_1:def 3 ;
hence f1 = f2 by A106, FINSEQ_1:13; :: thesis: verum