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) ex 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 )
let F be Group-like associative multMagma-Family of Seg n; :: thesis: for x being Element of (product F) ex 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 )
let x be Element of (product F); :: thesis: ex 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 )
set I = Seg n;
defpred S₁[ 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_ (product F)) +* (k,g) );
A1: for k being Nat st k in Seg n holds
ex z being Element of (product F) st S₁[k,z]

proof

let k be Nat; :: thesis: ( k in Seg n implies ex z being Element of (product F) st S₁[k,z] )
assume k in Seg n ; :: thesis: ex z being Element of (product F) st S₁[k,z]
then reconsider k0 = k as Element of Seg n ;
A2: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
A3: dom (Carrier F) = Seg n by PARTFUN1:def 2;
consider Rj being 1-sorted such that
A4: ( Rj = F . k0 & (Carrier F) . k0 = the carrier of Rj ) by PRALG_1:def 15;
reconsider g = x . k0 as Element of (F . k0) by A4, A3, A2, CARD_3:9;
(1_ (product F)) +* (k0,g) in ProjSet (F,k0) by Def1;
then reconsider z = (1_ (product F)) +* (k0,g) as Element of (product F) ;
take z ; :: thesis: S₁[k,z]
thus S₁[k,z] ; :: thesis: verum

end;

consider s being FinSequence of (product F) such that
A5: ( dom s = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,s . k] ) ) from FINSEQ_1:sch 5(A1);
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 A5, FINSEQ_1:def 3; :: 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_ (product F)) +* (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 A8, STRUCT_0:def 5; :: thesis: verum

end;

set y = Product s;
A9: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
A10: dom x = Seg n by A9, PARTFUN1:def 2;
A11: dom (Product s) = Seg n by A9, PARTFUN1:def 2;
A12: dom (1_ (product F)) = Seg n by A9, PARTFUN1:def 2;

now :: thesis: for t being object st t in dom x holds
x . t = (Product s) . t

let t be object ; :: thesis: ( t in dom x implies x . t = (Product s) . t )
assume t in dom x ; :: thesis: x . t = (Product s) . t
then A13: t in Seg n by A9, PARTFUN1:def 2;
then reconsider i = t as Nat ;
( 1 <= i & i <= n ) by A13, FINSEQ_1:1;
then A14: ex si being Element of (product F) st
( si = s . i & (Product s) . 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_ (product F)) +* (i1,g) ) by A13, A5;
hence x . t = (Product s) . t by A12, A14, FUNCT_7:31; :: thesis: verum

end;

hence x = Product s by A10, A11, FUNCT_1:2; :: thesis: verum