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 );
P0: S₁[ 0 ] ;
PN: 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 PN1: 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 PN2: ( 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 PN211N: len s = 1 by XXREAL_0:1, PN2;
then PN22: s = <*(s . 1)*> by FINSEQ_1:57;
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 PN24P: ( 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 PN2;
then 1 in dom s by FINSEQ_1:def 3;
then reconsider si = s . 1 as Element of (product F) by FINSEQ_2:13;
take si ; :: thesis: ( si = s . i & x . i = si . i )
thus ( si = s . i & x . i = si . i ) by PN24P, PN22, GROUP_4:12, PN2, PN211N, XXREAL_0:1; :: thesis: verum

end;

end;

suppose PN21: 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 PN211: 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 XREAL_1:15, PN2;
hence ( 1 <= len s & len s <= m & m <= n ) by PN2, PN211; :: 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 PN1, PN2; :: thesis: verum

end;

suppose PN212: 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 )

PN2120: len s = m + 1 by NAT_1:8, PN2, PN212;
LSLTN: len s <= n by PN2, NAT_1:8, PN212;
then len s in Seg n by PN2;
then reconsider ls = len s as Element of Seg n ;
set t = s | m;
LMMTM1: m < m + 1 by NAT_1:13;
dom s = Seg (m + 1) by PN2120, FINSEQ_1:def 3;
then Seg m c= dom s by FINSEQ_1:7, LMMTM1;
then dom (s | m) = Seg m by RELAT_1:91;
then LLTM: len (s | m) = m by FINSEQ_1:def 3;
LMMT1: 0 + 1 <= m by NAT_1:13, PN21;
P213: (m + 1) - 1 <= n - 0 by XREAL_1:15, PN2;
aa: ( dom s = Seg (len s) & dom (s | m) = Seg (len (s | m)) ) by FINSEQ_1:def 3;

P214: now

let k be Element of Seg n; :: thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) )
assume P215ttt: k in dom (s | m) ; :: thesis: (s | m) . k in ProjGroup (F,k)
then P215: (s | m) . k = s . k by FUNCT_1:70;
Seg (len (s | m)) c= Seg (len s) by LLTM, PN212, FINSEQ_1:7;
hence (s | m) . k in ProjGroup (F,k) by P215, PN2, P215ttt, aa; :: thesis: verum

end;

set y = Product (s | m);
P218: len s in Seg (len s) by PN2;
then reconsider sn = s . (len s) as Element of (product F) by aa, FINSEQ_2:13;
P216: s = (s | m) ^ <*sn*> by PN2120, FINSEQ_3:61;
P217: x = (Product (s | m)) * sn by GROUP_4:9, P216, PN2;
s . (len s) in ProjGroup (F,ls) by aa, PN2, P218;
then s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def 5;
then P218: s . (len s) in ProjSet (F,ls) by defPrjGroup;
set Gn = F . ls;
consider snn being Function, gn being Element of (F . ls) such that
P220: ( 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 P218, LMP1;
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 P222: ( 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 P223: i <> len s ; :: thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )

then P2231: i < len s by P222, XXREAL_0:1;
len s = (len (s | m)) + (len <*sn*>) by P216, FINSEQ_1:35
.= (len (s | m)) + 1 by FINSEQ_1:57 ;
then P2232: ( 1 <= i & i <= len (s | m) ) by P222, NAT_1:13, P2231;
then consider ti being Element of (product F) such that
P224: ( ti = (s | m) . i & (Product (s | m)) . i = ti . i ) by PN1, P213, P214, LLTM, LMMT1;
P227: (s | m) . i = s . i by FINSEQ_1:85, P2232, P216;
( 1 <= i & i <= n ) by P2232, XXREAL_0:2, P213, LLTM;
then reconsider ii = i as Element of Seg n by FINSEQ_1:3;
P226: sn . ii = 1_ (F . ii) by P220, P223;
consider Rii being 1-sorted such that
C3: ( Rii = F . ii & (Carrier F) . ii = the carrier of Rii ) by PRALG_1:def 13;
W0: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
Y0: dom (Carrier F) = Seg n by PARTFUN1:def 4;
reconsider tii = ti . i as Element of (F . ii) by C3, CARD_3:18, W0, Y0;
x . i = tii * (1_ (F . ii)) by GROUP_7:4, P224, P226, P217
.= ti . i by GROUP_1:def 5 ;
hence ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by P224, P227; :: thesis: verum

end;

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

P224: (Product (s | m)) . i = 1_ (F . ls) by P223, LMP400, P214, PN212, LLTM, LSLTN, P222;
x . i = (1_ (F . ls)) * gn by GROUP_7:4, P223, P224, P220, P217
.= sn . i by GROUP_1:def 5, P220, P223 ;
hence ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by P223; :: 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;

X1: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(P0, PN);
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 ASX: ( 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 )
Y1: ( 1 <= len s & len s <= n ) by ASX, NAT_1:14;
for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) by ASX;
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 ASX, Y1, X1; :: thesis: verum

end;