let n be non zero 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 S1[ 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: 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 (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 :: 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 ( 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;
A14: m in NAT by ORDINAL1:def 12;
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 A15: len (s | m) = m by FINSEQ_1:def 3, A14;
A16: 0 + 1 <= m by A8, NAT_1:13;
A17: (m + 1) - 1 <= n - 0 by A4, XREAL_1:13;
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 A15, A10, FINSEQ_1:5;
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 (product F) by A18, FINSEQ_2:11;
A23: s = (s | m) ^ <*sn*> by A11, FINSEQ_3:55;
A24: x = (Product (s | m)) * sn by A23, A4, GROUP_4:6;
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 A25, 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 A27: ( 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 A28: i <> len s ; :: thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )
then A29: i < len s by A27, XXREAL_0:1;
len s = (len (s | m)) + (len <*sn*>) by A23, FINSEQ_1:22
.= (len (s | m)) + 1 by FINSEQ_1:40 ;
then A30: ( 1 <= i & i <= len (s | m) ) by A27, A29, NAT_1:13;
then consider ti being Element of (product F) 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 A30, A23, FINSEQ_1:64;
( 1 <= i & i <= n ) by A30, A17, A15, XXREAL_0:2;
then reconsider ii = i as Element of Seg n by FINSEQ_1:1;
A33: sn . ii = 1_ (F . ii) by A26, A28;
consider Rii being 1-sorted such that
A34: ( Rii = F . ii & (Carrier F) . ii = the carrier of Rii ) by PRALG_1:def 15;
A35: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
A36: dom (Carrier F) = Seg n by PARTFUN1:def 2;
reconsider tii = ti . i as Element of (F . ii) by A34, A35, A36, CARD_3:9;
x . i = tii * (1_ (F . ii)) by A31, A33, A24, 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 A31, A32; :: thesis: verum
end;
suppose A37: i = len s ; :: thesis: ex si being Element of (product F) 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 A37, A38, A26, A24, GROUP_7:1
.= sn . i by A26, A37, GROUP_1:def 4 ;
hence ex si being Element of (product F) 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 (product F) 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 (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 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 (product F) st
( si = s . i & x . i = si . i )
A41: ( 1 <= len s & len s <= n ) by A40, NAT_1:14;
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 (product F) st
( si = s . i & x . i = si . i ) by A40, A41, A39; :: thesis: verum
end;