let n be non zero Nat; :: thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of () ex s being FinSequence of () st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )

let F be Group-like associative multMagma-Family of Seg n; :: thesis: for x being Element of () ex s being FinSequence of () st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )

let x be Element of (); :: thesis: ex s being FinSequence of () st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )

set I = Seg n;
defpred S1[ Nat, set ] means ex k being Element of Seg n ex g being Element of (F . k) st
( k = \$1 & x . k = g & \$2 = (1_ ()) +* (k,g) );
A1: for k being Nat st k in Seg n holds
ex z being Element of () st S1[k,z]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex z being Element of () st S1[k,z] )
assume k in Seg n ; :: thesis: ex z being Element of () st S1[k,z]
then reconsider k0 = k as Element of Seg n ;
A2: the carrier of () = product () by GROUP_7:def 2;
A3: dom () = Seg n by PARTFUN1:def 2;
consider Rj being 1-sorted such that
A4: ( Rj = F . k0 & () . k0 = the carrier of Rj ) by PRALG_1:def 13;
reconsider g = x . k0 as Element of (F . k0) by ;
(1_ ()) +* (k0,g) in ProjSet (F,k0) by Def1;
then reconsider z = (1_ ()) +* (k0,g) as Element of () ;
take z ; :: thesis: S1[k,z]
thus S1[k,z] ; :: thesis: verum
end;
consider s being FinSequence of () such that
A5: ( dom s = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s . k] ) ) from take s ; :: thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
n in NAT by ORDINAL1:def 12;
hence A6: len s = n by ; :: thesis: ( ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
thus A7: for k being Element of Seg n holds s . k in ProjGroup (F,k) :: thesis: x = Product s
proof
let k be Element of Seg n; :: thesis: s . k in ProjGroup (F,k)
ex k0 being Element of Seg n ex g being Element of (F . k0) st
( k0 = k & x . k0 = g & s . k = (1_ ()) +* (k0,g) ) by A5;
then A8: s . k in ProjSet (F,k) by Def1;
the carrier of (ProjGroup (F,k)) = ProjSet (F,k) by Def2;
hence s . k in ProjGroup (F,k) by ; :: thesis: verum
end;
set y = Product s;
A9: the carrier of () = product () by GROUP_7:def 2;
A10: dom x = Seg n by ;
A11: dom () = Seg n by ;
A12: dom (1_ ()) = Seg n by ;
now :: thesis: for t being object st t in dom x holds
x . t = () . t
let t be object ; :: thesis: ( t in dom x implies x . t = () . t )
assume t in dom x ; :: thesis: x . t = () . t
then A13: t in Seg n by ;
then reconsider i = t as Nat ;
( 1 <= i & i <= n ) by ;
then A14: ex si being Element of () st
( si = s . i & () . i = si . i ) by Th9, A6, A7;
ex i1 being Element of Seg n ex g being Element of (F . i1) st
( i1 = i & x . i1 = g & s . i = (1_ ()) +* (i1,g) ) by ;
hence x . t = () . t by ; :: thesis: verum
end;
hence x = Product s by ; :: thesis: verum