let n be non empty Nat; :: thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s being FinSequence of (product F) 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 (product F) 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 (product F)
for s being FinSequence of (product F) 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 (product F) st
( si = s . i & x . i = si . i )
defpred S₁[ Nat] means for x being Element of (product F)
for s being FinSequence of (product F) 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 (product F) st
( si = s . i & x . i = si . i );
A1: S₁[ 0 ] ;
A2: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: S₁[m] ; :: thesis: S₁[m + 1]
let x be Element of (product F); :: thesis: for s being FinSequence of (product F) 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 (product F) st
( si = s . i & x . i = si . i )
let s be FinSequence of (product F); :: 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 (product F) 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 (product F) 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 (product F) st
( si = s . i & x . i = si . i )

then A5: len s = 1 by A4, XXREAL_0:1;
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 (product F) 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 (product F) st
( si = s . i & x . i = si . i ) )
assume A7: ( 1 <= i & i <= len s ) ; :: thesis: ex si being Element of (product F) 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 (product F) by FINSEQ_2:11;
take si ; :: thesis: ( si = s . i & x . i = si . i )
thus ( si = s . i & x . i = si . i ) by A7, A6, A4, A5, GROUP_4:9, XXREAL_0:1; :: 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 (product F) st
( si = s . i & x . i = si . i )

now

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 (product F) st
( si = s . i & x . i = si . i )

( 1 <= len s & len s <= m & m <= n )

proof

(m + 1) - 1 <= n - 0 by A4, XREAL_1:13;
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 (product F) 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 (product F) st
( si = s . i & x . i = si . i )

A11: len s = m + 1 by A4, A10, NAT_1:8;
A12: len s <= n by A4, A10, NAT_1:8;
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;
dom s = Seg (m + 1) by A11, FINSEQ_1:def 3;
then Seg m c= dom s by A13, FINSEQ_1:5;
then dom (s | m) = Seg m by RELAT_1:62;
then A14: len (s | m) = m by FINSEQ_1:def 3;
A15: 0 + 1 <= m by A8, NAT_1:13;
A16: (m + 1) - 1 <= n - 0 by A4, XREAL_1:13;
A17: ( dom s = Seg (len s) & dom (s | m) = Seg (len (s | m)) ) by FINSEQ_1:def 3;

A18: now

let k be Element of Seg n; :: thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) )
assume A19: k in dom (s | m) ; :: thesis: (s | m) . k in ProjGroup (F,k)
then A20: (s | m) . k = s . k by FUNCT_1:47;
Seg (len (s | m)) c= Seg (len s) by A14, A10, FINSEQ_1:5;
hence (s | m) . k in ProjGroup (F,k) by A20, A4, A19, A17; :: thesis: verum

end;

set y = Product (s | m);
A21: len s in Seg (len s) by A4;
then reconsider sn = s . (len s) as Element of (product F) by A17, FINSEQ_2:11;
A22: s = (s | m) ^ <*sn*> by A11, FINSEQ_3:55;
A23: x = (Product (s | m)) * sn by A22, A4, GROUP_4:6;
s . (len s) in ProjGroup (F,ls) by A17, A4, A21;
then s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def 5;
then A24: 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
A25: ( 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 A24, Th2;
thus for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) 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 (product F) st
( si = s . i & x . i = si . i ) )
assume A26: ( 1 <= i & i <= len s ) ; :: thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )

per cases ( i <> len s or i = len s ) ;

suppose A27: i <> len s ; :: thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )

then A28: i < len s by A26, XXREAL_0:1;
len s = (len (s | m)) + (len <*sn*>) by A22, FINSEQ_1:22
.= (len (s | m)) + 1 by FINSEQ_1:40 ;
then A29: ( 1 <= i & i <= len (s | m) ) by A26, A28, NAT_1:13;
then consider ti being Element of (product F) such that
A30: ( ti = (s | m) . i & (Product (s | m)) . i = ti . i ) by A3, A16, A18, A14, A15;
A31: (s | m) . i = s . i by A29, A22, FINSEQ_1:64;
( 1 <= i & i <= n ) by A29, A16, A14, XXREAL_0:2;
then reconsider ii = i as Element of Seg n by FINSEQ_1:1;
A32: sn . ii = 1_ (F . ii) by A25, A27;
consider Rii being 1-sorted such that
A33: ( Rii = F . ii & (Carrier F) . ii = the carrier of Rii ) by PRALG_1:def 13;
A34: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
A35: dom (Carrier F) = Seg n by PARTFUN1:def 2;
reconsider tii = ti . i as Element of (F . ii) by A33, A34, A35, CARD_3:9;
x . i = tii * (1_ (F . ii)) by A30, A32, A23, GROUP_7:1
.= ti . i by GROUP_1:def 4 ;
hence ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A30, A31; :: thesis: verum

end;

suppose A36: i = len s ; :: thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )

A37: (Product (s | m)) . i = 1_ (F . ls) by A36, Th8, A18, A10, A14, A12, A26;
x . i = (1_ (F . ls)) * gn by A36, A37, A25, A23, GROUP_7:1
.= sn . i by A25, A36, GROUP_1:def 4 ;
hence ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A36; :: 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 (product F) st
( si = s . i & x . i = si . i ) ; :: thesis: verum

end;

end;

end;

A38: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A1, A2);
thus for x being Element of (product F)
for s being FinSequence of (product F) 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 (product F) st
( si = s . i & x . i = si . i ) :: thesis: verum

proof

let x be Element of (product F); :: thesis: for s being FinSequence of (product F) 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 (product F) st
( si = s . i & x . i = si . i )
let s be FinSequence of (product F); :: 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 (product F) st
( si = s . i & x . i = si . i ) )
assume A39: ( 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 (product F) st
( si = s . i & x . i = si . i )
A40: ( 1 <= len s & len s <= n ) by A39, NAT_1:14;
for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) by A39;
hence for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A39, A40, A38; :: thesis: verum

end;