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 ()
for s being FinSequence of () 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 ()
for s being FinSequence of () 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 ()
for s being FinSequence of () 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 ()
for s being FinSequence of () 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 ()
for s being FinSequence of () 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 S1[ Nat] means for x being Element of ()
for s being FinSequence of () 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: S1[ 0 ]
proof
let x be Element of (); :: thesis: for s being FinSequence of () 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 (); :: 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 () by A3;
then A4: x = 1_ () by ;
J in Seg n by A1;
hence x . J = 1_ GJ by ; :: thesis: verum
end;
A5: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A6: S1[m] ; :: thesis: S1[m + 1]
let x be Element of (); :: thesis: for s being FinSequence of () 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 (); :: 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 ;
( 1 <= len s & len s <= n ) by ;
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 ;
k in dom s by ;
hence (s | m) . k in ProjGroup (F,k) by ; :: thesis: verum
end;
set y = Product (s | m);
A13: m in NAT by ORDINAL1:def 12;
dom s = Seg (m + 1) by ;
then Seg m c= dom s by ;
then A14: dom (s | m) = Seg m by RELAT_1:62;
then A15: len (s | m) = m by ;
A16: len (s | m) = (len s) - 1 by ;
A17: (Product (s | m)) . J = 1_ GJ by ;
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 () by FINSEQ_2:11;
A19: (len (s | m)) + 1 = len s by ;
len ((s | m) ^ <*sn*>) = len s by ;
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
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 A22: k in Seg ((len (s | m)) + 1) by ;
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 ;
case A23: 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 ;
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 ; :: thesis: verum
end;
end;
end;
hence s . k = ((s | m) ^ <*sn*>) . k ; :: thesis: verum
end;
hence s = (s | m) ^ <*sn*> by ; :: thesis: verum
end;
A24: x = (Product (s | m)) * sn by ;
s . (len s) in ProjGroup (F,ls) by ;
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 ;
thus x . J = 1_ GJ :: thesis: verum
proof
reconsider J0 = J as Element of Seg n by ;
A27: snn . J0 = 1_ (F . J0) by ;
thus x . J = (1_ (F . J0)) * (1_ (F . J0)) by
.= 1_ GJ by ; :: thesis: verum
end;
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A2, A5);
hence for x being Element of ()
for s being FinSequence of () 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