(len s2) - 1 > 1 - 1
by A2, XREAL_1:9;

then reconsider l99 = (len s2) - 1 as Element of NAT by INT_1:3;

(len s2) + 1 > 1 + 1 by A2, XREAL_1:6;

then len s2 >= 2 by NAT_1:13;

then A3: (len s2) - 1 >= 2 - 1 by XREAL_1:9;

(len s1) - 1 > 1 - 1 by A1, XREAL_1:9;

then reconsider l9 = (len s1) - 1 as Element of NAT by INT_1:3;

defpred S_{1}[ set , object ] means for i, j being Nat

for H1, H2, H3 being StableSubgroup of G holds

( ( $1 = ((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 $2 = H1 "\/" (H2 /\ H3) ) & ( $1 = (((len s1) - 1) * ((len s2) - 1)) + 1 implies $2 = (1). G ) );

(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;

then A4: l99 / l99 = 1 by XCMPLX_1:60;

(len s1) + 1 > 1 + 1 by A1, XREAL_1:6;

then len s1 >= 2 by NAT_1:13;

then A5: (len s1) - 1 >= 2 - 1 by XREAL_1:9;

then A6: (((len s1) - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by A3, XREAL_1:6;

reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by A5, A3, INT_1:3;

A7: 1 in Seg l by A6;

A8: for k being Nat st k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds

for i, j being Nat holds

( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 )

ex x being object st S_{1}[k,x]

A33: ( dom f = Seg l & ( for k being Nat st k in Seg l holds

S_{1}[k,f . k] ) )
from FINSEQ_1:sch 1(A21);

for k being Nat st k in dom f holds

f . k in the_stable_subgroups_of G

l in Seg l by A6;

then S_{1}[l,f . l]
by A33;

then A38: f . (len f) = (1). G by A33, FINSEQ_1:def 3;

A39: for i being Nat

for s1 being CompositionSeries of G

for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds

s1 . (i + 1) is normal StableSubgroup of H

for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1

then ((len s1) - 1) * ((len s2) - 1) > 0 * ((len s2) - 1) by XREAL_1:68;

then 1 <> l ;

then consider i, j being Nat such that

A84: 1 = ((i - 1) * ((len s2) - 1)) + j and

A85: 1 <= i and

A86: i <= (len s1) - 1 and

A87: 1 <= j and

A88: j <= (len s2) - 1 by A1, A2, A7, Lm44;

set i9 = i - 1;

i - 1 >= 1 - 1 by A85, XREAL_1:9;

then reconsider i9 = i - 1 as Element of NAT by INT_1:3;

reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A85, A86, A87, A88, Th111;

1 mod l99 = ((i9 * l99) + j) mod l99 by A84;

then A89: 1 mod l99 = j mod l99 by NAT_D:21;

A90: j = 1 then A92: H3 = (Omega). G by Def28;

(i9 * l99) / l99 = 0 / l99 by A84, A90;

then i9 * 1 = 0 by A4, XCMPLX_1:74;

then A93: H2 = (Omega). G by Def28;

f . 1 = H1 "\/" (H2 /\ H3) by A33, A7, A84, A85, A86, A87, A88;

then f . 1 = H1 "\/" ((Omega). G) by A93, A92, Th19;

then f . 1 = (Omega). G by Th34;

then reconsider f = f as CompositionSeries of G by A38, A46, Def28;

take f ; :: 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )

let k, i, j be Nat; :: thesis: 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )

let H1, H2, H3 be StableSubgroup of G; :: thesis: ( ( 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )

A94: for k, i, j being Nat st k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds

k in Seg l

then reconsider l99 = (len s2) - 1 as Element of NAT by INT_1:3;

(len s2) + 1 > 1 + 1 by A2, XREAL_1:6;

then len s2 >= 2 by NAT_1:13;

then A3: (len s2) - 1 >= 2 - 1 by XREAL_1:9;

(len s1) - 1 > 1 - 1 by A1, XREAL_1:9;

then reconsider l9 = (len s1) - 1 as Element of NAT by INT_1:3;

defpred S

for H1, H2, H3 being StableSubgroup of G holds

( ( $1 = ((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 $2 = H1 "\/" (H2 /\ H3) ) & ( $1 = (((len s1) - 1) * ((len s2) - 1)) + 1 implies $2 = (1). G ) );

(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;

then A4: l99 / l99 = 1 by XCMPLX_1:60;

(len s1) + 1 > 1 + 1 by A1, XREAL_1:6;

then len s1 >= 2 by NAT_1:13;

then A5: (len s1) - 1 >= 2 - 1 by XREAL_1:9;

then A6: (((len s1) - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by A3, XREAL_1:6;

reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by A5, A3, INT_1:3;

A7: 1 in Seg l by A6;

A8: for k being Nat st k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds

for i, j being Nat holds

( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 )

proof

A21:
for k being Nat st k in Seg l holds
let k be Nat; :: thesis: ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies for i, j being Nat holds

( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 ) )

assume A9: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: for i, j being Nat holds

( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 )

assume 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: contradiction

then consider i, j being Nat such that

A10: k = ((i - 1) * ((len s2) - 1)) + j and

A11: 1 <= i and

A12: i <= (len s1) - 1 and

A13: 1 <= j and

A14: j <= (len s2) - 1 ;

set i9 = i - 1;

i - 1 >= 1 - 1 by A11, XREAL_1:9;

then reconsider i9 = i - 1 as Element of NAT by INT_1:3;

A15: 1 mod l99 = ((l9 * l99) + 1) mod l99 by NAT_D:21

.= ((i9 * l99) + j) mod l99 by A9, A10

.= j mod l99 by NAT_D:21 ;

j = 1

l99 / l99 = 1 by A13, A14, XCMPLX_1:60;

then A20: l9 * 1 = i9 * 1 by A19, XCMPLX_1:74;

(- 1) + i < 0 + i by XREAL_1:6;

hence contradiction by A12, A20; :: thesis: verum

end;( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 ) )

assume A9: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: for i, j being Nat holds

( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 )

assume 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: contradiction

then consider i, j being Nat such that

A10: k = ((i - 1) * ((len s2) - 1)) + j and

A11: 1 <= i and

A12: i <= (len s1) - 1 and

A13: 1 <= j and

A14: j <= (len s2) - 1 ;

set i9 = i - 1;

i - 1 >= 1 - 1 by A11, XREAL_1:9;

then reconsider i9 = i - 1 as Element of NAT by INT_1:3;

A15: 1 mod l99 = ((l9 * l99) + 1) mod l99 by NAT_D:21

.= ((i9 * l99) + j) mod l99 by A9, A10

.= j mod l99 by NAT_D:21 ;

j = 1

proof
end;

then A19:
l9 * (l99 / l99) = (i9 * l99) / l99
by A9, A10, XCMPLX_1:74;per cases
( j = l99 or j <> l99 )
;

end;

suppose A16:
j = l99
; :: thesis: j = 1

assume
j <> 1
; :: thesis: contradiction

then 1 < l99 by A13, A16, XXREAL_0:1;

then 1 = j mod l99 by A15, NAT_D:24;

hence contradiction by A16, NAT_D:25; :: thesis: verum

end;then 1 < l99 by A13, A16, XXREAL_0:1;

then 1 = j mod l99 by A15, NAT_D:24;

hence contradiction by A16, NAT_D:25; :: thesis: verum

suppose
j <> l99
; :: thesis: j = 1

end;

end;

l99 / l99 = 1 by A13, A14, XCMPLX_1:60;

then A20: l9 * 1 = i9 * 1 by A19, XCMPLX_1:74;

(- 1) + i < 0 + i by XREAL_1:6;

hence contradiction by A12, A20; :: thesis: verum

ex x being object st S

proof

consider f being FinSequence such that
let k be Nat; :: thesis: ( k in Seg l implies ex x being object st S_{1}[k,x] )

assume A22: k in Seg l ; :: thesis: ex x being object st S_{1}[k,x]

end;assume A22: k in Seg l ; :: thesis: ex x being object st S

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, A22, Lm44;

end;

( 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, A22, Lm44;

suppose A23:
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: ex x being object st S_{1}[k,x]

( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ; :: thesis: ex x being object st S

then consider i, j being Nat such that

A24: k = ((i - 1) * ((len s2) - 1)) + j and

A25: 1 <= i and

A26: i <= (len s1) - 1 and

A27: ( 1 <= j & j <= (len s2) - 1 ) ;

reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A25, A26, A27, Th111;

take x = H1 "\/" (H2 /\ H3); :: thesis: S_{1}[k,x]

_{1}[k,x]
; :: thesis: verum

end;A24: k = ((i - 1) * ((len s2) - 1)) + j and

A25: 1 <= i and

A26: i <= (len s1) - 1 and

A27: ( 1 <= j & j <= (len s2) - 1 ) ;

reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A25, A26, A27, Th111;

take x = H1 "\/" (H2 /\ H3); :: thesis: S

now :: thesis: for i1, j1 being Nat

for H1, H2, H3 being StableSubgroup of G holds

( ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G ) )

hence
Sfor H1, H2, H3 being StableSubgroup of G holds

( ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G ) )

let i1, j1 be Nat; :: thesis: for H1, H2, H3 being StableSubgroup of G holds

( ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G ) )

let H1, H2, H3 be StableSubgroup of G; :: thesis: ( ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G ) )

thus ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) :: thesis: ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G )

hence x = (1). G by A8, A23; :: thesis: verum

end;( ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G ) )

let H1, H2, H3 be StableSubgroup of G; :: thesis: ( ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G ) )

thus ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) :: thesis: ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies x = (1). G )

proof

assume
k = (((len s1) - 1) * ((len s2) - 1)) + 1
; :: thesis: x = (1). G
assume that

A28: k = ((i1 - 1) * ((len s2) - 1)) + j1 and

A29: 1 <= i1 and

i1 <= (len s1) - 1 and

A30: ( 1 <= j1 & j1 <= (len s2) - 1 ) ; :: thesis: ( not H1 = s1 . (i1 + 1) or not H2 = s1 . i1 or not H3 = s2 . j1 or x = H1 "\/" (H2 /\ H3) )

assume A31: ( H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 ) ; :: thesis: x = H1 "\/" (H2 /\ H3)

i = i1 by A2, A24, A25, A27, A28, A29, A30, Lm45;

hence x = H1 "\/" (H2 /\ H3) by A24, A28, A31; :: thesis: verum

end;A28: k = ((i1 - 1) * ((len s2) - 1)) + j1 and

A29: 1 <= i1 and

i1 <= (len s1) - 1 and

A30: ( 1 <= j1 & j1 <= (len s2) - 1 ) ; :: thesis: ( not H1 = s1 . (i1 + 1) or not H2 = s1 . i1 or not H3 = s2 . j1 or x = H1 "\/" (H2 /\ H3) )

assume A31: ( H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 ) ; :: thesis: x = H1 "\/" (H2 /\ H3)

i = i1 by A2, A24, A25, A27, A28, A29, A30, Lm45;

hence x = H1 "\/" (H2 /\ H3) by A24, A28, A31; :: thesis: verum

hence x = (1). G by A8, A23; :: thesis: verum

A33: ( dom f = Seg l & ( for k being Nat st k in Seg l holds

S

for k being Nat st k in dom f holds

f . k in the_stable_subgroups_of G

proof

then reconsider f = f as FinSequence of the_stable_subgroups_of G by FINSEQ_2:12;
let k be Nat; :: thesis: ( k in dom f implies f . k in the_stable_subgroups_of G )

assume A34: k in dom f ; :: thesis: f . k in the_stable_subgroups_of G

then A35: for 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) ) by A33;

end;assume A34: k in dom f ; :: thesis: f . k in the_stable_subgroups_of G

then A35: for 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) ) by A33;

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, A33, A34, Lm44;

end;

( 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, A33, A34, 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: f . k in the_stable_subgroups_of G

( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ; :: thesis: f . k in the_stable_subgroups_of G

then consider i, j being Nat such that

A36: k = ((i - 1) * ((len s2) - 1)) + j and

A37: ( 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 A37, Th111;

f . k = H1 "\/" (H2 /\ H3) by A33, A34, A36, A37;

hence f . k in the_stable_subgroups_of G by Def11; :: thesis: verum

end;A36: k = ((i - 1) * ((len s2) - 1)) + j and

A37: ( 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 A37, Th111;

f . k = H1 "\/" (H2 /\ H3) by A33, A34, A36, A37;

hence f . k in the_stable_subgroups_of G by Def11; :: thesis: verum

l in Seg l by A6;

then S

then A38: f . (len f) = (1). G by A33, FINSEQ_1:def 3;

A39: for i being Nat

for s1 being CompositionSeries of G

for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds

s1 . (i + 1) is normal StableSubgroup of H

proof

A46:
for k being Nat st k in dom f & k + 1 in dom f holds
let i be Nat; :: thesis: for s1 being CompositionSeries of G

for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds

s1 . (i + 1) is normal StableSubgroup of H

let s1 be CompositionSeries of G; :: thesis: for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds

s1 . (i + 1) is normal StableSubgroup of H

let H be GroupWithOperators of O; :: thesis: ( 1 <= i & i <= (len s1) - 1 & H = s1 . i implies s1 . (i + 1) is normal StableSubgroup of H )

assume that

A40: 1 <= i and

A41: i <= (len s1) - 1 ; :: thesis: ( not H = s1 . i or s1 . (i + 1) is normal StableSubgroup of H )

A42: 0 + i <= 1 + i by XREAL_1:6;

A43: i + 1 <= ((len s1) - 1) + 1 by A41, XREAL_1:6;

then i <= len s1 by A42, XXREAL_0:2;

then i in Seg (len s1) by A40;

then A44: i in dom s1 by FINSEQ_1:def 3;

reconsider H1 = s1 . i, H2 = s1 . (i + 1) as StableSubgroup of G by A40, A41, Th111;

assume A45: H = s1 . i ; :: thesis: s1 . (i + 1) is normal StableSubgroup of H

1 <= i + 1 by A40, A42, XXREAL_0:2;

then i + 1 in Seg (len s1) by A43;

then i + 1 in dom s1 by FINSEQ_1:def 3;

then H2 is normal StableSubgroup of H1 by A44, Def28;

hence s1 . (i + 1) is normal StableSubgroup of H by A45; :: thesis: verum

end;for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds

s1 . (i + 1) is normal StableSubgroup of H

let s1 be CompositionSeries of G; :: thesis: for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds

s1 . (i + 1) is normal StableSubgroup of H

let H be GroupWithOperators of O; :: thesis: ( 1 <= i & i <= (len s1) - 1 & H = s1 . i implies s1 . (i + 1) is normal StableSubgroup of H )

assume that

A40: 1 <= i and

A41: i <= (len s1) - 1 ; :: thesis: ( not H = s1 . i or s1 . (i + 1) is normal StableSubgroup of H )

A42: 0 + i <= 1 + i by XREAL_1:6;

A43: i + 1 <= ((len s1) - 1) + 1 by A41, XREAL_1:6;

then i <= len s1 by A42, XXREAL_0:2;

then i in Seg (len s1) by A40;

then A44: i in dom s1 by FINSEQ_1:def 3;

reconsider H1 = s1 . i, H2 = s1 . (i + 1) as StableSubgroup of G by A40, A41, Th111;

assume A45: H = s1 . i ; :: thesis: s1 . (i + 1) is normal StableSubgroup of H

1 <= i + 1 by A40, A42, XXREAL_0:2;

then i + 1 in Seg (len s1) by A43;

then i + 1 in dom s1 by FINSEQ_1:def 3;

then H2 is normal StableSubgroup of H1 by A44, Def28;

hence s1 . (i + 1) is normal StableSubgroup of H by A45; :: thesis: verum

for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1

proof

( (len s1) - 1 > 1 - 1 & (len s2) - 1 > 1 - 1 )
by A1, A2, XREAL_1:9;
let k be Nat; :: thesis: ( k in dom f & k + 1 in dom f implies for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1 )

assume A47: k in dom f ; :: thesis: ( not k + 1 in dom f or for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1 )

set k9 = k + 1;

assume A48: k + 1 in dom f ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1

then k + 1 <= l by A33, FINSEQ_1:1;

then k <> l by NAT_1:13;

then consider i, j being Nat such that

A49: k = ((i - 1) * ((len s2) - 1)) + j and

A50: 1 <= i and

A51: i <= (len s1) - 1 and

A52: 1 <= j and

A53: j <= (len s2) - 1 by A1, A2, A33, A47, Lm44;

reconsider H19 = s1 . (i + 1), H29 = s1 . i, H39 = s2 . j as strict StableSubgroup of G by A50, A51, A52, A53, Th111;

A54: f . k = H19 "\/" (H29 /\ H39) by A33, A47, A49, A50, A51, A52, A53;

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = f . k & H2 = f . (k + 1) implies H2 is normal StableSubgroup of H1 )

assume A55: H1 = f . k ; :: thesis: ( not H2 = f . (k + 1) or H2 is normal StableSubgroup of H1 )

A56: H19 is normal StableSubgroup of H29 by A39, A50, A51;

assume A57: H2 = f . (k + 1) ; :: thesis: H2 is normal StableSubgroup of H1

end;H2 is normal StableSubgroup of H1 )

assume A47: k in dom f ; :: thesis: ( not k + 1 in dom f or for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1 )

set k9 = k + 1;

assume A48: k + 1 in dom f ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds

H2 is normal StableSubgroup of H1

then k + 1 <= l by A33, FINSEQ_1:1;

then k <> l by NAT_1:13;

then consider i, j being Nat such that

A49: k = ((i - 1) * ((len s2) - 1)) + j and

A50: 1 <= i and

A51: i <= (len s1) - 1 and

A52: 1 <= j and

A53: j <= (len s2) - 1 by A1, A2, A33, A47, Lm44;

reconsider H19 = s1 . (i + 1), H29 = s1 . i, H39 = s2 . j as strict StableSubgroup of G by A50, A51, A52, A53, Th111;

A54: f . k = H19 "\/" (H29 /\ H39) by A33, A47, A49, A50, A51, A52, A53;

let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = f . k & H2 = f . (k + 1) implies H2 is normal StableSubgroup of H1 )

assume A55: H1 = f . k ; :: thesis: ( not H2 = f . (k + 1) or H2 is normal StableSubgroup of H1 )

A56: H19 is normal StableSubgroup of H29 by A39, A50, A51;

assume A57: H2 = f . (k + 1) ; :: thesis: H2 is normal StableSubgroup of H1

per cases
( j <> (len s2) - 1 or j = (len s2) - 1 )
;

end;

suppose A58:
j <> (len s2) - 1
; :: thesis: H2 is normal StableSubgroup of H1

reconsider j9 = j + 1 as Nat ;

j < (len s2) - 1 by A53, A58, XXREAL_0:1;

then A59: j9 <= (len s2) - 1 by INT_1:7;

reconsider H399 = s2 . j9 as strict StableSubgroup of G by A52, A53, Th111;

0 + j <= 1 + j by XREAL_1:6;

then A60: 1 <= j9 by A52, XXREAL_0:2;

A61: H399 is normal StableSubgroup of H39 by A39, A52, A53;

k + 1 = ((i - 1) * ((len s2) - 1)) + j9 by A49;

then H2 = H19 "\/" (H29 /\ H399) by A33, A48, A50, A51, A57, A59, A60;

hence H2 is normal StableSubgroup of H1 by A55, A56, A54, A61, Th92; :: thesis: verum

end;j < (len s2) - 1 by A53, A58, XXREAL_0:1;

then A59: j9 <= (len s2) - 1 by INT_1:7;

reconsider H399 = s2 . j9 as strict StableSubgroup of G by A52, A53, Th111;

0 + j <= 1 + j by XREAL_1:6;

then A60: 1 <= j9 by A52, XXREAL_0:2;

A61: H399 is normal StableSubgroup of H39 by A39, A52, A53;

k + 1 = ((i - 1) * ((len s2) - 1)) + j9 by A49;

then H2 = H19 "\/" (H29 /\ H399) by A33, A48, A50, A51, A57, A59, A60;

hence H2 is normal StableSubgroup of H1 by A55, A56, A54, A61, Th92; :: thesis: verum

suppose A62:
j = (len s2) - 1
; :: thesis: H2 is normal StableSubgroup of H1

end;

per cases
( i <> (len s1) - 1 or i = (len s1) - 1 )
;

end;

suppose A63:
i <> (len s1) - 1
; :: thesis: H2 is normal StableSubgroup of H1

set i9 = i + 1;

A64: 0 + (i + 1) <= 1 + (i + 1) by XREAL_1:6;

set j9 = 1;

H19 is StableSubgroup of H1 by A55, A54, Th35;

then H19 is Subgroup of H1 by Def7;

then A65: the carrier of H19 c= the carrier of H1 by GROUP_2:def 5;

1 + 1 <= i + 1 by A50, XREAL_1:6;

then A66: 1 <= i + 1 by XXREAL_0:2;

i < l9 by A51, A63, XXREAL_0:1;

then A67: i + 1 <= l9 by NAT_1:13;

then A68: (i + 1) + 1 <= ((len s1) - 1) + 1 by XREAL_1:6;

then i + 1 <= len s1 by A64, XXREAL_0:2;

then i + 1 in Seg (len s1) by A66;

then A69: i + 1 in dom s1 by FINSEQ_1:def 3;

(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;

then A70: l99 >= 0 + 1 by NAT_1:13;

then reconsider H199 = s1 . ((i + 1) + 1), H299 = s1 . (i + 1), H399 = s2 . 1 as strict StableSubgroup of G by A67, A66, Th111;

1 <= (i + 1) + 1 by A66, A64, XXREAL_0:2;

then (i + 1) + 1 in Seg (len s1) by A68;

then (i + 1) + 1 in dom s1 by FINSEQ_1:def 3;

then A71: H199 is normal StableSubgroup of H299 by A69, Def28;

then A73: the carrier of H299 = the carrier of H299 /\ the carrier of ((Omega). G) by XBOOLE_1:28;

A74: H399 = (Omega). G by Def28;

k + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by A49, A62;

then H2 = H199 "\/" (H299 /\ H399) by A33, A48, A57, A67, A66, A70;

then H2 = H199 "\/" H299 by A74, A73, Th18;

then A75: H2 = H19 by A71, Th36;

H29 /\ H39 is StableSubgroup of H29 by Lm33;

then A76: H1 is StableSubgroup of H29 by A55, A56, A54, Th37;

then A77: H1 is Subgroup of H29 by Def7;

end;A64: 0 + (i + 1) <= 1 + (i + 1) by XREAL_1:6;

set j9 = 1;

H19 is StableSubgroup of H1 by A55, A54, Th35;

then H19 is Subgroup of H1 by Def7;

then A65: the carrier of H19 c= the carrier of H1 by GROUP_2:def 5;

1 + 1 <= i + 1 by A50, XREAL_1:6;

then A66: 1 <= i + 1 by XXREAL_0:2;

i < l9 by A51, A63, XXREAL_0:1;

then A67: i + 1 <= l9 by NAT_1:13;

then A68: (i + 1) + 1 <= ((len s1) - 1) + 1 by XREAL_1:6;

then i + 1 <= len s1 by A64, XXREAL_0:2;

then i + 1 in Seg (len s1) by A66;

then A69: i + 1 in dom s1 by FINSEQ_1:def 3;

(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;

then A70: l99 >= 0 + 1 by NAT_1:13;

then reconsider H199 = s1 . ((i + 1) + 1), H299 = s1 . (i + 1), H399 = s2 . 1 as strict StableSubgroup of G by A67, A66, Th111;

1 <= (i + 1) + 1 by A66, A64, XXREAL_0:2;

then (i + 1) + 1 in Seg (len s1) by A68;

then (i + 1) + 1 in dom s1 by FINSEQ_1:def 3;

then A71: H199 is normal StableSubgroup of H299 by A69, Def28;

now :: thesis: for x being object st x in the carrier of H299 holds

x in the carrier of ((Omega). G)

then
the carrier of H299 c= the carrier of ((Omega). G)
;x in the carrier of ((Omega). G)

let x be object ; :: thesis: ( x in the carrier of H299 implies x in the carrier of ((Omega). G) )

H299 is Subgroup of G by Def7;

then A72: the carrier of H299 c= the carrier of G by GROUP_2:def 5;

assume x in the carrier of H299 ; :: thesis: x in the carrier of ((Omega). G)

hence x in the carrier of ((Omega). G) by A72; :: thesis: verum

end;H299 is Subgroup of G by Def7;

then A72: the carrier of H299 c= the carrier of G by GROUP_2:def 5;

assume x in the carrier of H299 ; :: thesis: x in the carrier of ((Omega). G)

hence x in the carrier of ((Omega). G) by A72; :: thesis: verum

then A73: the carrier of H299 = the carrier of H299 /\ the carrier of ((Omega). G) by XBOOLE_1:28;

A74: H399 = (Omega). G by Def28;

k + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by A49, A62;

then H2 = H199 "\/" (H299 /\ H399) by A33, A48, A57, A67, A66, A70;

then H2 = H199 "\/" H299 by A74, A73, Th18;

then A75: H2 = H19 by A71, Th36;

H29 /\ H39 is StableSubgroup of H29 by Lm33;

then A76: H1 is StableSubgroup of H29 by A55, A56, A54, Th37;

then A77: H1 is Subgroup of H29 by Def7;

now :: thesis: for H9 being strict Subgroup of H1 st H9 = multMagma(# the carrier of H2, the multF of H2 #) holds

H9 is normal

hence
H2 is normal StableSubgroup of H1
by A55, A54, A75, Def10, Th35; :: thesis: verumH9 is normal

let H9 be strict Subgroup of H1; :: thesis: ( H9 = multMagma(# the carrier of H2, the multF of H2 #) implies H9 is normal )

assume A78: H9 = multMagma(# the carrier of H2, the multF of H2 #) ; :: thesis: H9 is normal

end;assume A78: H9 = multMagma(# the carrier of H2, the multF of H2 #) ; :: thesis: H9 is normal

now :: thesis: for a being Element of H1 holds a * H9 c= H9 * a

hence
H9 is normal
by GROUP_3:118; :: thesis: verumlet a be Element of H1; :: thesis: a * H9 c= H9 * a

reconsider a9 = a as Element of H29 by A76, Th2;

end;reconsider a9 = a as Element of H29 by A76, Th2;

now :: thesis: for x being object st x in a * H9 holds

x in H9 * a

hence
a * H9 c= H9 * a
; :: thesis: verumx in H9 * a

reconsider H1s9 = multMagma(# the carrier of H19, the multF of H19 #) as normal Subgroup of H29 by A56, Lm6;

let x be object ; :: thesis: ( x in a * H9 implies x in H9 * a )

assume x in a * H9 ; :: thesis: x in H9 * a

then consider b being Element of H1 such that

A79: x = a * b and

A80: b in H9 by GROUP_2:103;

set b9 = b;

A81: H1 is Subgroup of H29 by A76, Def7;

then reconsider b9 = b as Element of H29 by GROUP_2:42;

x = a9 * b9 by A79, A81, GROUP_2:43;

then ( a9 * H1s9 c= H1s9 * a9 & x in a9 * H1s9 ) by A75, A78, A80, GROUP_2:103, GROUP_3:118;

then consider b99 being Element of H29 such that

A82: x = b99 * a9 and

A83: b99 in H1s9 by GROUP_2:104;

b99 in the carrier of H19 by A83, STRUCT_0:def 5;

then reconsider b99 = b99 as Element of H1 by A65;

x = b99 * a by A77, A82, GROUP_2:43;

hence x in H9 * a by A75, A78, A83, GROUP_2:104; :: thesis: verum

end;let x be object ; :: thesis: ( x in a * H9 implies x in H9 * a )

assume x in a * H9 ; :: thesis: x in H9 * a

then consider b being Element of H1 such that

A79: x = a * b and

A80: b in H9 by GROUP_2:103;

set b9 = b;

A81: H1 is Subgroup of H29 by A76, Def7;

then reconsider b9 = b as Element of H29 by GROUP_2:42;

x = a9 * b9 by A79, A81, GROUP_2:43;

then ( a9 * H1s9 c= H1s9 * a9 & x in a9 * H1s9 ) by A75, A78, A80, GROUP_2:103, GROUP_3:118;

then consider b99 being Element of H29 such that

A82: x = b99 * a9 and

A83: b99 in H1s9 by GROUP_2:104;

b99 in the carrier of H19 by A83, STRUCT_0:def 5;

then reconsider b99 = b99 as Element of H1 by A65;

x = b99 * a by A77, A82, GROUP_2:43;

hence x in H9 * a by A75, A78, A83, GROUP_2:104; :: thesis: verum

suppose
i = (len s1) - 1
; :: thesis: H2 is normal StableSubgroup of H1

then H2 =
(1). G
by A33, A48, A49, A57, A62

.= (1). H1 by Th15 ;

hence H2 is normal StableSubgroup of H1 ; :: thesis: verum

end;.= (1). H1 by Th15 ;

hence H2 is normal StableSubgroup of H1 ; :: thesis: verum

then ((len s1) - 1) * ((len s2) - 1) > 0 * ((len s2) - 1) by XREAL_1:68;

then 1 <> l ;

then consider i, j being Nat such that

A84: 1 = ((i - 1) * ((len s2) - 1)) + j and

A85: 1 <= i and

A86: i <= (len s1) - 1 and

A87: 1 <= j and

A88: j <= (len s2) - 1 by A1, A2, A7, Lm44;

set i9 = i - 1;

i - 1 >= 1 - 1 by A85, XREAL_1:9;

then reconsider i9 = i - 1 as Element of NAT by INT_1:3;

reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A85, A86, A87, A88, Th111;

1 mod l99 = ((i9 * l99) + j) mod l99 by A84;

then A89: 1 mod l99 = j mod l99 by NAT_D:21;

A90: j = 1 then A92: H3 = (Omega). G by Def28;

(i9 * l99) / l99 = 0 / l99 by A84, A90;

then i9 * 1 = 0 by A4, XCMPLX_1:74;

then A93: H2 = (Omega). G by Def28;

f . 1 = H1 "\/" (H2 /\ H3) by A33, A7, A84, A85, A86, A87, A88;

then f . 1 = H1 "\/" ((Omega). G) by A93, A92, Th19;

then f . 1 = (Omega). G by Th34;

then reconsider f = f as CompositionSeries of G by A38, A46, Def28;

take f ; :: 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )

let k, i, j be Nat; :: thesis: 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )

let H1, H2, H3 be StableSubgroup of G; :: thesis: ( ( 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 f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )

A94: for k, i, j being Nat st k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds

k in Seg l

proof

let k, i, j be Nat; :: thesis: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 implies k in Seg l )

assume A95: k = ((i - 1) * ((len s2) - 1)) + j ; :: thesis: ( not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 or k in Seg l )

assume that

A96: 1 <= i and

A97: i <= (len s1) - 1 ; :: thesis: ( not 1 <= j or not j <= (len s2) - 1 or k in Seg l )

assume that

A98: 1 <= j and

A99: j <= (len s2) - 1 ; :: thesis: k in Seg l

i - 1 <= l9 - 1 by A97, XREAL_1:9;

then (i - 1) * l99 <= (l9 - 1) * l99 by XREAL_1:64;

then ( 0 + (l9 * l99) <= 1 + (l9 * l99) & k <= ((l9 * l99) - (1 * l99)) + l99 ) by A95, A99, XREAL_1:7;

then A100: k <= (((len s1) - 1) * ((len s2) - 1)) + 1 by XXREAL_0:2;

1 - 1 <= i - 1 by A96, XREAL_1:9;

then 0 + 1 <= ((i - 1) * ((len s2) - 1)) + j by A3, A98, XREAL_1:7;

hence k in Seg l by A95, A100; :: thesis: verum

end;assume A95: k = ((i - 1) * ((len s2) - 1)) + j ; :: thesis: ( not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 or k in Seg l )

assume that

A96: 1 <= i and

A97: i <= (len s1) - 1 ; :: thesis: ( not 1 <= j or not j <= (len s2) - 1 or k in Seg l )

assume that

A98: 1 <= j and

A99: j <= (len s2) - 1 ; :: thesis: k in Seg l

i - 1 <= l9 - 1 by A97, XREAL_1:9;

then (i - 1) * l99 <= (l9 - 1) * l99 by XREAL_1:64;

then ( 0 + (l9 * l99) <= 1 + (l9 * l99) & k <= ((l9 * l99) - (1 * l99)) + l99 ) by A95, A99, XREAL_1:7;

then A100: k <= (((len s1) - 1) * ((len s2) - 1)) + 1 by XXREAL_0:2;

1 - 1 <= i - 1 by A96, XREAL_1:9;

then 0 + 1 <= ((i - 1) * ((len s2) - 1)) + j by A3, A98, XREAL_1:7;

hence k in Seg l by A95, A100; :: thesis: verum

now :: thesis: ( 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 f . k = H1 "\/" (H2 /\ H3) )

hence
( 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 f . k = H1 "\/" (H2 /\ H3) )
; :: thesis: ( ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )assume that

A101: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) and

A102: ( H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j ) ; :: thesis: f . k = H1 "\/" (H2 /\ H3)

k in Seg l by A94, A101;

hence f . k = H1 "\/" (H2 /\ H3) by A33, A101, A102; :: thesis: verum

end;A101: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) and

A102: ( H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j ) ; :: thesis: f . k = H1 "\/" (H2 /\ H3)

k in Seg l by A94, A101;

hence f . k = H1 "\/" (H2 /\ H3) by A33, A101, A102; :: thesis: verum

now :: thesis: ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G )

hence
( ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 )
by A33, FINSEQ_1:def 3; :: thesis: verumassume A103:
k = (((len s1) - 1) * ((len s2) - 1)) + 1
; :: thesis: f . k = (1). G

then k in Seg l by A6;

hence f . k = (1). G by A33, A103; :: thesis: verum

end;then k in Seg l by A6;

hence f . k = (1). G by A33, A103; :: thesis: verum