(len s2) - 1 > 1 - 1 by ;
then reconsider l99 = (len s2) - 1 as Element of NAT by INT_1:3;
(len s2) + 1 > 1 + 1 by ;
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 ;
then reconsider l9 = (len s1) - 1 as Element of NAT by INT_1:3;
defpred S1[ 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 ;
then A4: l99 / l99 = 1 by XCMPLX_1:60;
(len s1) + 1 > 1 + 1 by ;
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 ;
reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by ;
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
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 ;
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
.= j mod l99 by NAT_D:21 ;
j = 1
proof
per cases ( j = l99 or j <> l99 ) ;
suppose A16: j = l99 ; :: thesis: j = 1
assume j <> 1 ; :: thesis: contradiction
then 1 < l99 by ;
then 1 = j mod l99 by ;
hence contradiction by A16, NAT_D:25; :: thesis: verum
end;
suppose j <> l99 ; :: thesis: j = 1
then j < l99 by ;
then A17: j mod l99 = j by NAT_D:24;
per cases ( 1 = l99 or 1 <> l99 ) ;
suppose 1 = l99 ; :: thesis: j = 1
hence j = 1 by ; :: thesis: verum
end;
suppose A18: 1 <> l99 ; :: thesis: j = 1
1 <= l99 by ;
then 1 < l99 by ;
hence j = 1 by ; :: thesis: verum
end;
end;
end;
end;
end;
then A19: l9 * (l99 / l99) = (i9 * l99) / l99 by ;
l99 / l99 = 1 by ;
then A20: l9 * 1 = i9 * 1 by ;
(- 1) + i < 0 + i by XREAL_1:6;
hence contradiction by A12, A20; :: thesis: verum
end;
A21: for k being Nat st k in Seg l holds
ex x being object st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg l implies ex x being object st S1[k,x] )
assume A22: k in Seg l ; :: thesis: ex x being object st S1[k,x]
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;
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 S1[k,x]
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 ;
take x = H1 "\/" (H2 /\ H3); :: thesis: S1[k,x]
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 ) )
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 )
proof
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 ; :: thesis: verum
end;
assume k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: x = (1). G
hence x = (1). G by ; :: thesis: verum
end;
hence S1[k,x] ; :: thesis: verum
end;
suppose A32: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis: ex x being object st S1[k,x]
take (1). G ; :: thesis: S1[k, (1). G]
thus S1[k, (1). G] by ; :: thesis: verum
end;
end;
end;
consider f being FinSequence such that
A33: ( dom f = Seg l & ( for k being Nat st k in Seg l holds
S1[k,f . k] ) ) from for k being Nat st k in dom f holds
f . k in the_stable_subgroups_of G
proof
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:
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;
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:
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 ;
f . k = H1 "\/" (H2 /\ H3) by A33, A34, A36, A37;
hence f . k in the_stable_subgroups_of G by Def11; :: thesis: verum
end;
suppose k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis:
end;
end;
end;
then reconsider f = f as FinSequence of the_stable_subgroups_of G by FINSEQ_2:12;
l in Seg l by A6;
then S1[l,f . l] by A33;
then A38: f . (len f) = (1). G by ;
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
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 ;
then i <= len s1 by ;
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 ;
assume A45: H = s1 . i ; :: thesis: s1 . (i + 1) is normal StableSubgroup of H
1 <= i + 1 by ;
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 ;
hence s1 . (i + 1) is normal StableSubgroup of H by A45; :: thesis: verum
end;
A46: for k being Nat st k in dom f & k + 1 in dom f holds
for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds
H2 is normal StableSubgroup of H1
proof
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 ;
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 ;
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 ;
assume A57: H2 = f . (k + 1) ; :: thesis: H2 is normal StableSubgroup of H1
per cases ( j <> (len s2) - 1 or j = (len s2) - 1 ) ;
suppose A58: j <> (len s2) - 1 ; :: thesis: H2 is normal StableSubgroup of H1
reconsider j9 = j + 1 as Nat ;
j < (len s2) - 1 by ;
then A59: j9 <= (len s2) - 1 by INT_1:7;
reconsider H399 = s2 . j9 as strict StableSubgroup of G by ;
0 + j <= 1 + j by XREAL_1:6;
then A60: 1 <= j9 by ;
A61: H399 is normal StableSubgroup of H39 by ;
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;
suppose A62: j = (len s2) - 1 ; :: thesis: H2 is normal StableSubgroup of H1
per cases ( i <> (len s1) - 1 or i = (len s1) - 1 ) ;
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 ;
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 ;
then A66: 1 <= i + 1 by XXREAL_0:2;
i < l9 by ;
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 ;
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 ;
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 ;
1 <= (i + 1) + 1 by ;
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 ;
now :: thesis: for x being object st x in the carrier of H299 holds
x in the carrier of ()
let x be object ; :: thesis: ( x in the carrier of H299 implies x in the carrier of () )
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 ()
hence x in the carrier of () by A72; :: thesis: verum
end;
then the carrier of H299 c= the carrier of () ;
then A73: the carrier of H299 = the carrier of H299 /\ the carrier of () by XBOOLE_1:28;
A74: H399 = (Omega). G by Def28;
k + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by ;
then H2 = H199 "\/" (H299 /\ H399) by A33, A48, A57, A67, A66, A70;
then H2 = H199 "\/" H299 by ;
then A75: H2 = H19 by ;
H29 /\ H39 is StableSubgroup of H29 by Lm33;
then A76: H1 is StableSubgroup of H29 by ;
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
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
now :: thesis: for a being Element of H1 holds a * H9 c= H9 * a
let a be Element of H1; :: thesis: a * H9 c= H9 * a
reconsider a9 = a as Element of H29 by ;
now :: thesis: for x being object st x in a * H9 holds
x in H9 * a
reconsider H1s9 = multMagma(# the carrier of H19, the multF of H19 #) as normal Subgroup of H29 by ;
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 ;
then reconsider b9 = b as Element of H29 by GROUP_2:42;
x = a9 * b9 by ;
then ( a9 * H1s9 c= H1s9 * a9 & x in a9 * H1s9 ) by ;
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 ;
then reconsider b99 = b99 as Element of H1 by A65;
x = b99 * a by ;
hence x in H9 * a by ; :: thesis: verum
end;
hence a * H9 c= H9 * a ; :: thesis: verum
end;
hence H9 is normal by GROUP_3:118; :: thesis: verum
end;
hence H2 is normal StableSubgroup of H1 by ; :: thesis: verum
end;
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;
end;
end;
end;
end;
( (len s1) - 1 > 1 - 1 & (len s2) - 1 > 1 - 1 ) by ;
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 ;
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 ;
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
proof
per cases ( l99 = 1 or l99 <> 1 ) ;
suppose l99 = 1 ; :: thesis: j = 1
hence j = 1 by ; :: thesis: verum
end;
suppose l99 <> 1 ; :: thesis: j = 1
then 1 < l99 by ;
then A91: 1 = j mod l99 by ;
then j <> l99 by NAT_D:25;
then l99 > j by ;
hence j = 1 by ; :: thesis: verum
end;
end;
end;
then A92: H3 = (Omega). G by Def28;
(i9 * l99) / l99 = 0 / l99 by ;
then i9 * 1 = 0 by ;
then A93: H2 = (Omega). G by Def28;
f . 1 = H1 "\/" (H2 /\ H3) by A33, A7, A84, A85, A86, A87, A88;
then f . 1 = H1 "\/" () by ;
then f . 1 = (Omega). G by Th34;
then reconsider f = f as CompositionSeries of G by ;
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 ;
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 ;
then A100: k <= (((len s1) - 1) * ((len s2) - 1)) + 1 by XXREAL_0:2;
1 - 1 <= i - 1 by ;
then 0 + 1 <= ((i - 1) * ((len s2) - 1)) + j by ;
hence k in Seg l by ; :: thesis: verum
end;
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) )
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 ;
hence f . k = H1 "\/" (H2 /\ H3) by ; :: thesis: verum
end;
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 )
now :: thesis: ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G )
assume 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 ; :: thesis: verum
end;
hence ( ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 ) by ; :: thesis: verum