let n be non zero Nat; :: thesis: for F being Group-like associative multMagma-Family of Seg n

for J being Nat

for GJ being Group st 1 <= J & J <= n & GJ = F . J holds

for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let F be Group-like associative multMagma-Family of Seg n; :: thesis: for J being Nat

for GJ being Group st 1 <= J & J <= n & GJ = F . J holds

for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let J be Nat; :: thesis: for GJ being Group st 1 <= J & J <= n & GJ = F . J holds

for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let GJ be Group; :: thesis: ( 1 <= J & J <= n & GJ = F . J implies for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ )

assume A1: ( 1 <= J & J <= n & GJ = F . J ) ; :: thesis: for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

defpred S_{1}[ Nat] means for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & len s = $1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ;

A2: S_{1}[ 0 ]
_{1}[m] holds

S_{1}[m + 1]
_{1}[m]
from NAT_1:sch 2(A2, A5);

hence for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ ; :: thesis: verum

for J being Nat

for GJ being Group st 1 <= J & J <= n & GJ = F . J holds

for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let F be Group-like associative multMagma-Family of Seg n; :: thesis: for J being Nat

for GJ being Group st 1 <= J & J <= n & GJ = F . J holds

for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let J be Nat; :: thesis: for GJ being Group st 1 <= J & J <= n & GJ = F . J holds

for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let GJ be Group; :: thesis: ( 1 <= J & J <= n & GJ = F . J implies for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ )

assume A1: ( 1 <= J & J <= n & GJ = F . J ) ; :: thesis: for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

defpred S

for s being FinSequence of (product F) st len s < J & len s = $1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ;

A2: S

proof

A5:
for m being Nat st S
let x be Element of (product F); :: thesis: for s being FinSequence of (product F) st len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let s be FinSequence of (product F); :: thesis: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ )

assume A3: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s ) ; :: thesis: x . J = 1_ GJ

s = <*> the carrier of (product F) by A3;

then A4: x = 1_ (product F) by A3, GROUP_4:8;

J in Seg n by A1;

hence x . J = 1_ GJ by A1, A4, GROUP_7:6; :: thesis: verum

end;s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let s be FinSequence of (product F); :: thesis: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ )

assume A3: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s ) ; :: thesis: x . J = 1_ GJ

s = <*> the carrier of (product F) by A3;

then A4: x = 1_ (product F) by A3, GROUP_4:8;

J in Seg n by A1;

hence x . J = 1_ GJ by A1, A4, GROUP_7:6; :: thesis: verum

S

proof

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

assume A6: S_{1}[m]
; :: thesis: S_{1}[m + 1]

let x be Element of (product F); :: thesis: for s being FinSequence of (product F) st len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let s be FinSequence of (product F); :: thesis: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ )

assume A7: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s ) ; :: thesis: x . J = 1_ GJ

A8: m < m + 1 by NAT_1:13;

A9: 1 <= len s by A7, NAT_1:11;

( 1 <= len s & len s <= n ) by A7, A1, NAT_1:11, XXREAL_0:2;

then len s in Seg n ;

then reconsider ls = len s as Element of Seg n ;

set t = s | m;

A13: m in NAT by ORDINAL1:def 12;

dom s = Seg (m + 1) by A7, FINSEQ_1:def 3;

then Seg m c= dom s by A8, FINSEQ_1:5;

then A14: dom (s | m) = Seg m by RELAT_1:62;

then A15: len (s | m) = m by FINSEQ_1:def 3, A13;

A16: len (s | m) = (len s) - 1 by A14, A7, FINSEQ_1:def 3, A13;

A17: (Product (s | m)) . J = 1_ GJ by A6, A10, A16, A7, XREAL_1:51;

len s in Seg (len s) by A9;

then A18: len s in dom s by FINSEQ_1:def 3;

then reconsider sn = s . (len s) as Element of (product F) by FINSEQ_2:11;

A19: (len (s | m)) + 1 = len s by A14, A7, FINSEQ_1:def 3, A13;

len ((s | m) ^ <*sn*>) = len s by A19, FINSEQ_2:16;

then A20: dom ((s | m) ^ <*sn*>) = Seg (len s) by FINSEQ_1:def 3

.= dom s by FINSEQ_1:def 3 ;

A21: s = (s | m) ^ <*sn*>

s . (len s) in ProjGroup (F,ls) by A7, A18;

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;

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 x . J = 1_ GJ :: thesis: verum

end;assume A6: S

let x be Element of (product F); :: thesis: for s being FinSequence of (product F) st len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ

let s be FinSequence of (product F); :: thesis: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ )

assume A7: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s ) ; :: thesis: x . J = 1_ GJ

A8: m < m + 1 by NAT_1:13;

A9: 1 <= len s by A7, NAT_1:11;

( 1 <= len s & len s <= n ) by A7, A1, NAT_1:11, XXREAL_0:2;

then len s in Seg n ;

then reconsider ls = len s as Element of Seg n ;

set t = s | m;

A10: 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 A11: k in dom (s | m) ; :: thesis: (s | m) . k in ProjGroup (F,k)

A12: (s | m) . k = s . k by A11, FUNCT_1:47;

k in dom s by A11, RELAT_1:57;

hence (s | m) . k in ProjGroup (F,k) by A12, A7; :: thesis: verum

end;assume A11: k in dom (s | m) ; :: thesis: (s | m) . k in ProjGroup (F,k)

A12: (s | m) . k = s . k by A11, FUNCT_1:47;

k in dom s by A11, RELAT_1:57;

hence (s | m) . k in ProjGroup (F,k) by A12, A7; :: thesis: verum

A13: m in NAT by ORDINAL1:def 12;

dom s = Seg (m + 1) by A7, FINSEQ_1:def 3;

then Seg m c= dom s by A8, FINSEQ_1:5;

then A14: dom (s | m) = Seg m by RELAT_1:62;

then A15: len (s | m) = m by FINSEQ_1:def 3, A13;

A16: len (s | m) = (len s) - 1 by A14, A7, FINSEQ_1:def 3, A13;

A17: (Product (s | m)) . J = 1_ GJ by A6, A10, A16, A7, XREAL_1:51;

len s in Seg (len s) by A9;

then A18: len s in dom s by FINSEQ_1:def 3;

then reconsider sn = s . (len s) as Element of (product F) by FINSEQ_2:11;

A19: (len (s | m)) + 1 = len s by A14, A7, FINSEQ_1:def 3, A13;

len ((s | m) ^ <*sn*>) = len s by A19, FINSEQ_2:16;

then A20: dom ((s | m) ^ <*sn*>) = Seg (len s) by FINSEQ_1:def 3

.= dom s by FINSEQ_1:def 3 ;

A21: s = (s | m) ^ <*sn*>

proof

A24:
x = (Product (s | m)) * sn
by A21, A7, GROUP_4:6;
for k being Nat st k in dom s holds

s . k = ((s | m) ^ <*sn*>) . k

end;s . k = ((s | m) ^ <*sn*>) . k

proof

hence
s = (s | m) ^ <*sn*>
by A20, FINSEQ_1:13; :: thesis: verum
let k be Nat; :: thesis: ( k in dom s implies s . k = ((s | m) ^ <*sn*>) . k )

assume k in dom s ; :: thesis: s . k = ((s | m) ^ <*sn*>) . k

then A22: k in Seg ((len (s | m)) + 1) by A19, FINSEQ_1:def 3;

end;assume k in dom s ; :: thesis: s . k = ((s | m) ^ <*sn*>) . k

then A22: k in Seg ((len (s | m)) + 1) by A19, FINSEQ_1:def 3;

now :: thesis: ( ( k in Seg (len (s | m)) & s . k = ((s | m) ^ <*sn*>) . k ) or ( k = (len (s | m)) + 1 & s . k = ((s | m) ^ <*sn*>) . k ) )end;

hence
s . k = ((s | m) ^ <*sn*>) . k
; :: thesis: verumper cases
( k in Seg (len (s | m)) or k = (len (s | m)) + 1 )
by A22, FINSEQ_2:7;

end;

s . (len s) in ProjGroup (F,ls) by A7, A18;

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;

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 x . J = 1_ GJ :: thesis: verum

hence for x being Element of (product F)

for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds

s . k in ProjGroup (F,k) ) & x = Product s holds

x . J = 1_ GJ ; :: thesis: verum