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_{1}[ 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_{1}[k,z]

A5: ( dom s = Seg n & ( for k being Nat st k in Seg n holds

S_{1}[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

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;

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

( 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

proof

consider s being FinSequence of (product F) such that
let k be Nat; :: thesis: ( k in Seg n implies ex z being Element of (product F) st S_{1}[k,z] )

assume k in Seg n ; :: thesis: ex z being Element of (product F) st S_{1}[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 13;

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_{1}[k,z]

thus S_{1}[k,z]
; :: thesis: verum

end;assume k in Seg n ; :: thesis: ex z being Element of (product F) st S

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 13;

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

thus S

A5: ( dom s = Seg n & ( for k being Nat st k in Seg n holds

S

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

set y = Product s;
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;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

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

hence
x = Product s
by A10, A11, FUNCT_1:2; :: thesis: verumx . 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;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