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 S_{1}[ 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_{1}[ 0 ]
;

A2: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[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

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

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

A2: for m being Nat st S

S

proof

A39:
for m being Nat holds S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A3: S_{1}[m]
; :: thesis: S_{1}[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 )

end;assume A3: S

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 )
;

end;

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 )

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

end;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;( 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

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 )

ex si being Element of (product F) st

( si = s . i & x . i = si . i ) ; :: thesis: verum

end;

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 )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 )

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

end;

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 )

ex si being Element of (product F) st

( si = s . i & x . i = si . i )

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

ex si being Element of (product F) st

( si = s . i & x . i = si . i ) by A3, A4; :: thesis: verum

end;proof

hence
for i being Nat st 1 <= i & i <= len s holds
(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 ( 1 <= len s & len s <= m & m <= n ) by A4, A9; :: thesis: verum

ex si being Element of (product F) st

( si = s . i & x . i = si . i ) by A3, A4; :: thesis: verum

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 )

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;

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

end;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)

set y = Product (s | m);(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;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

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 )

end;( 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 )
;

end;

suppose A28:
i <> len s
; :: thesis: ex si being Element of (product F) st

( si = s . i & x . i = si . i )

( 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 13;

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;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 13;

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

suppose A37:
i = len s
; :: thesis: ex si being Element of (product F) st

( si = s . i & x . i = si . i )

( 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;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

ex si being Element of (product F) st

( si = s . i & x . i = si . i ) ; :: thesis: verum

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;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