let n be non zero Nat; :: thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of ()
for s being FinSequence of () st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i )

let F be Group-like associative multMagma-Family of Seg n; :: thesis: for x being Element of ()
for s being FinSequence of () st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i )

defpred S1[ Nat] means for x being Element of ()
for s being FinSequence of () st 1 <= len s & len s <= \$1 & \$1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i );
A1: S1[ 0 ] ;
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; :: thesis: S1[m + 1]
let x be Element of (); :: thesis: for s being FinSequence of () st 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )

let s be FinSequence of (); :: thesis: ( 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s implies for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i ) )

assume A4: ( 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s ) ; :: thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )

per cases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; :: thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )

then A5: len s = 1 by ;
then A6: s = <*(s . 1)*> by FINSEQ_1:40;
thus for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i ) :: thesis: verum
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len s implies ex si being Element of () st
( si = s . i & x . i = si . i ) )

assume A7: ( 1 <= i & i <= len s ) ; :: thesis: ex si being Element of () st
( si = s . i & x . i = si . i )

1 in Seg (len s) by A4;
then 1 in dom s by FINSEQ_1:def 3;
then reconsider si = s . 1 as Element of () by FINSEQ_2:11;
take si ; :: thesis: ( si = s . i & x . i = si . i )
thus ( si = s . i & x . i = si . i ) by ; :: thesis: verum
end;
end;
suppose A8: m <> 0 ; :: thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )

now :: thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )
per cases ( len s <= m or len s > m ) ;
suppose A9: len s <= m ; :: thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )

( 1 <= len s & len s <= m & m <= n )
proof
(m + 1) - 1 <= n - 0 by ;
hence ( 1 <= len s & len s <= m & m <= n ) by A4, A9; :: thesis: verum
end;
hence for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i ) by A3, A4; :: thesis: verum
end;
suppose A10: len s > m ; :: thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i )

A11: len s = m + 1 by ;
A12: len s <= n by ;
then len s in Seg n by A4;
then reconsider ls = len s as Element of Seg n ;
set t = s | m;
A13: m < m + 1 by NAT_1:13;
A14: m in NAT by ORDINAL1:def 12;
dom s = Seg (m + 1) by ;
then Seg m c= dom s by ;
then dom (s | m) = Seg m by RELAT_1:62;
then A15: len (s | m) = m by ;
A16: 0 + 1 <= m by ;
A17: (m + 1) - 1 <= n - 0 by ;
A18: ( dom s = Seg (len s) & dom (s | m) = Seg (len (s | m)) ) by FINSEQ_1:def 3;
A19: now :: thesis: for k being Element of Seg n st k in dom (s | m) holds
(s | m) . k in ProjGroup (F,k)
let k be Element of Seg n; :: thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) )
assume A20: k in dom (s | m) ; :: thesis: (s | m) . k in ProjGroup (F,k)
then A21: (s | m) . k = s . k by FUNCT_1:47;
Seg (len (s | m)) c= Seg (len s) by ;
hence (s | m) . k in ProjGroup (F,k) by A21, A4, A20, A18; :: thesis: verum
end;
set y = Product (s | m);
A22: len s in Seg (len s) by A4;
then reconsider sn = s . (len s) as Element of () by ;
A23: s = (s | m) ^ <*sn*> by ;
A24: x = (Product (s | m)) * sn by ;
s . (len s) in ProjGroup (F,ls) by A18, A4, A22;
then s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def 5;
then A25: s . (len s) in ProjSet (F,ls) by Def2;
set Gn = F . ls;
consider snn being Function, gn being Element of (F . ls) such that
A26: ( snn = sn & dom snn = Seg n & snn . ls = gn & ( for k being Element of Seg n st k <> ls holds
snn . k = 1_ (F . k) ) ) by ;
thus for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i ) :: thesis: verum
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len s implies ex si being Element of () st
( si = s . i & x . i = si . i ) )

assume A27: ( 1 <= i & i <= len s ) ; :: thesis: ex si being Element of () st
( si = s . i & x . i = si . i )

per cases ( i <> len s or i = len s ) ;
suppose A28: i <> len s ; :: thesis: ex si being Element of () st
( si = s . i & x . i = si . i )

then A29: i < len s by ;
len s = (len (s | m)) + (len <*sn*>) by
.= (len (s | m)) + 1 by FINSEQ_1:40 ;
then A30: ( 1 <= i & i <= len (s | m) ) by ;
then consider ti being Element of () such that
A31: ( ti = (s | m) . i & (Product (s | m)) . i = ti . i ) by A3, A17, A19, A15, A16;
A32: (s | m) . i = s . i by ;
( 1 <= i & i <= n ) by ;
then reconsider ii = i as Element of Seg n by FINSEQ_1:1;
A33: sn . ii = 1_ (F . ii) by ;
consider Rii being 1-sorted such that
A34: ( Rii = F . ii & () . ii = the carrier of Rii ) by PRALG_1:def 13;
A35: the carrier of () = product () by GROUP_7:def 2;
A36: dom () = Seg n by PARTFUN1:def 2;
reconsider tii = ti . i as Element of (F . ii) by ;
x . i = tii * (1_ (F . ii)) by
.= ti . i by GROUP_1:def 4 ;
hence ex si being Element of () st
( si = s . i & x . i = si . i ) by ; :: thesis: verum
end;
suppose A37: i = len s ; :: thesis: ex si being Element of () st
( si = s . i & x . i = si . i )

A38: (Product (s | m)) . i = 1_ (F . ls) by A37, Th8, A19, A10, A15, A12, A27;
x . i = (1_ (F . ls)) * gn by
.= sn . i by ;
hence ex si being Element of () st
( si = s . i & x . i = si . i ) by A37; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence for i being Nat st 1 <= i & i <= len s holds
ex si being Element of () st
( si = s . i & x . i = si . i ) ; :: thesis: verum
end;
end;
end;
A39: for m being Nat holds S1[m] from NAT_1:sch 2(A1, A2);
thus for x being Element of ()
for s being FinSequence of () st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i ) :: thesis: verum
proof
let x be Element of (); :: thesis: for s being FinSequence of () st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i )

let s be FinSequence of (); :: thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s implies for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i ) )

assume A40: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) ; :: thesis: for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i )

A41: ( 1 <= len s & len s <= n ) by ;
for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) by A40;
hence for i being Nat st 1 <= i & i <= n holds
ex si being Element of () st
( si = s . i & x . i = si . i ) by ; :: thesis: verum
end;