let n be non empty 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₁[ 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₁[ 0 ]

proof

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, FINSEQ_1:1;
hence x . J = 1_ GJ by A1, A4, GROUP_7:6; :: thesis: verum

end;

A5: 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 A6: S₁[m] ; :: thesis: S₁[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;

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

set y = Product (s | m);
dom s = Seg (m + 1) by A7, FINSEQ_1:def 3;
then Seg m c= dom s by A8, FINSEQ_1:5;
then A13: dom (s | m) = Seg m by RELAT_1:62;
then A14: len (s | m) = m by FINSEQ_1:def 3;
A15: len (s | m) = (len s) - 1 by A13, A7, FINSEQ_1:def 3;
A16: (Product (s | m)) . J = 1_ GJ by A6, A10, A15, A7, XREAL_1:51;
len s in Seg (len s) by A9;
then A17: 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;
A18: (len (s | m)) + 1 = len s by A13, A7, FINSEQ_1:def 3;
len ((s | m) ^ <*sn*>) = len s by A18, FINSEQ_2:16;
then A19: dom ((s | m) ^ <*sn*>) = Seg (len s) by FINSEQ_1:def 3
.= dom s by FINSEQ_1:def 3 ;
A20: s = (s | m) ^ <*sn*>

proof

for k being Nat st k in dom s holds
s . k = ((s | m) ^ <*sn*>) . k

proof

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 A21: k in Seg ((len (s | m)) + 1) by A18, 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 ) )

per cases ( k in Seg (len (s | m)) or k = (len (s | m)) + 1 ) by A21, FINSEQ_2:7;

case A22: k in Seg (len (s | m)) ; :: thesis: s . k = ((s | m) ^ <*sn*>) . k

then k in dom (s | m) by FINSEQ_1:def 3;
then ((s | m) ^ <*sn*>) . k = (s | m) . k by FINSEQ_1:def 7
.= s . k by A22, A14, FUNCT_1:49 ;
hence s . k = ((s | m) ^ <*sn*>) . k ; :: thesis: verum

end;

case k = (len (s | m)) + 1 ; :: thesis: s . k = ((s | m) ^ <*sn*>) . k

hence s . k = ((s | m) ^ <*sn*>) . k by A18, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

hence s . k = ((s | m) ^ <*sn*>) . k ; :: thesis: verum

end;

hence s = (s | m) ^ <*sn*> by A19, FINSEQ_1:13; :: thesis: verum

end;

A23: x = (Product (s | m)) * sn by A20, A7, GROUP_4:6;
s . (len s) in ProjGroup (F,ls) by A7, A17;
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;
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 x . J = 1_ GJ :: thesis: verum

proof

reconsider J0 = J as Element of Seg n by A1, FINSEQ_1:1;
A26: snn . J0 = 1_ (F . J0) by A25, A7;
thus x . J = (1_ (F . J0)) * (1_ (F . J0)) by A16, A25, A26, A23, A1, GROUP_7:1
.= 1_ GJ by A1, GROUP_1:def 4 ; :: thesis: verum

end;

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(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