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)
for s, t 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 & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let F be Group-like associative multMagma-Family of Seg n; :: thesis: for x being Element of (product F)
for s, t 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 & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let x be Element of (product F); :: thesis: for s, t 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 & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let s, t be FinSequence of (product F); :: thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t implies s = t )
set I = Seg n;
assume that
A1: len s = n and
A2: for k being Element of Seg n holds s . k in ProjGroup (F,k) and
A3: x = Product s and
A4: len t = n and
A5: for k being Element of Seg n holds t . k in ProjGroup (F,k) and
A6: x = Product t ; :: thesis: s = t
now :: thesis: for i being Nat st 1 <= i & i <= n holds
s . i = t . i
let i be Nat; :: thesis: ( 1 <= i & i <= n implies s . i = t . i )
assume A7: ( 1 <= i & i <= n ) ; :: thesis: s . i = t . i
then reconsider i0 = i as Element of Seg n by FINSEQ_1:1;
consider si being Element of (product F) such that
A8: ( si = s . i & x . i = si . i ) by A1, A2, A3, A7, Th9;
consider ti being Element of (product F) such that
A9: ( ti = t . i & x . i = ti . i ) by A4, A5, A6, A7, Th9;
s . i0 in ProjGroup (F,i0) by A2;
then s . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def 5;
then A10: s . i0 in ProjSet (F,i0) by Def2;
consider sn being Function, gn being Element of (F . i0) such that
A11: ( sn = si & dom sn = Seg n & sn . i0 = gn & ( for k being Element of Seg n st k <> i0 holds
sn . k = 1_ (F . k) ) ) by A8, A10, Th2;
t . i0 in ProjGroup (F,i0) by A5;
then t . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def 5;
then A12: t . i0 in ProjSet (F,i0) by Def2;
consider tn being Function, fn being Element of (F . i0) such that
A13: ( tn = ti & dom tn = Seg n & tn . i0 = fn & ( for k being Element of Seg n st k <> i0 holds
tn . k = 1_ (F . k) ) ) by A9, A12, Th2;
now :: thesis: for x being object st x in dom sn holds
sn . x = tn . x
let x be object ; :: thesis: ( x in dom sn implies sn . b1 = tn . b1 )
assume x in dom sn ; :: thesis: sn . b1 = tn . b1
then reconsider j = x as Element of Seg n by A11;
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: sn . b1 = tn . b1
hence sn . x = tn . x by A8, A9, A11, A13; :: thesis: verum
end;
suppose A14: j <> i ; :: thesis: sn . b1 = tn . b1
then sn . j = 1_ (F . j) by A11;
hence sn . x = tn . x by A14, A13; :: thesis: verum
end;
end;
end;
hence s . i = t . i by A8, A9, A11, A13, FUNCT_1:2; :: thesis: verum
end;
hence s = t by A1, A4; :: thesis: verum