:: FINSOP_1 semantic presentation
begin
definition
let D be non empty set ;
let F be FinSequence of D;
let g be BinOp of D;
assume A1: ( g is having_a_unity or len F >= 1 ) ;
funcg "**" F -> Element of D means :Def1: :: FINSOP_1:def 1
it = the_unity_wrt g if ( g is having_a_unity & len F = 0 )
otherwise ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & it = f . (len F) );
existence
( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) )
proof
now__::_thesis:_(_(_g_is_having_a_unity_&_len_F_=_0_implies_ex_b1_being_Element_of_D_st_b1_=_the_unity_wrt_g_)_&_(_(_not_g_is_having_a_unity_or_not_len_F_=_0_)_implies_ex_b1_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_
(_f_._1_=_F_._1_&_(_for_n_being_Element_of_NAT_st_0_<>_n_&_n_<_len_F_holds_
f_._(n_+_1)_=_g_._((f_._n),(F_._(n_+_1)))_)_&_b1_=_f_._(len_F)_)_)_)
percases ( len F = 0 or len F <> 0 ) ;
suppose len F = 0 ; ::_thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) )
hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) by A1; ::_thesis: verum
end;
supposeA2: len F <> 0 ; ::_thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) )
defpred S1[ Element of NAT ] means for F being FinSequence of D st len F = $1 & len F <> 0 holds
ex d being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) );
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let F be FinSequence of D; ::_thesis: ( len F = k + 1 & len F <> 0 implies ex d being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) )
assume that
A5: len F = k + 1 and
len F <> 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
reconsider G = F | (Seg k) as FinSequence of D by FINSEQ_1:18;
A6: len G = k by A5, FINSEQ_3:53;
now__::_thesis:_ex_d_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_
(_f_._1_=_F_._1_&_(_for_n_being_Element_of_NAT_st_0_<>_n_&_n_<_len_F_holds_
f_._(n_+_1)_=_g_._((f_._n),(F_._(n_+_1)))_)_&_d_=_f_._(len_F)_)
percases ( len G = 0 or len G <> 0 ) ;
supposeA7: len G = 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
set f = NAT --> (F . 1);
A8: rng (NAT --> (F . 1)) c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (NAT --> (F . 1)) or x in D )
assume x in rng (NAT --> (F . 1)) ; ::_thesis: x in D
then ex y being set st
( y in dom (NAT --> (F . 1)) & (NAT --> (F . 1)) . y = x ) by FUNCT_1:def_3;
then A9: x = F . 1 by FUNCOP_1:7;
1 in dom F by A5, A6, A7, FINSEQ_3:25;
then A10: x in rng F by A9, FUNCT_1:def_3;
rng F c= D by FINSEQ_1:def_4;
hence x in D by A10; ::_thesis: verum
end;
dom (NAT --> (F . 1)) = NAT by FUNCOP_1:13;
then reconsider f = NAT --> (F . 1) as Function of NAT,D by A8, RELSET_1:4;
take d = f . 1; ::_thesis: ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
take f = f; ::_thesis: ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
thus f . 1 = F . 1 by FUNCOP_1:7; ::_thesis: ( ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
thus for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) by A5, A6, A7, NAT_1:14; ::_thesis: d = f . (len F)
thus d = f . (len F) by A5, A6, A7; ::_thesis: verum
end;
supposeA11: len G <> 0 ; ::_thesis: ex a being Element of D ex h being Function of NAT,D st
( h . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
reconsider j = len F as Element of NAT ;
1 <= len F by A5, NAT_1:12;
then len F in dom F by FINSEQ_3:25;
then A12: F . (len F) in rng F by FUNCT_1:def_3;
rng F c= D by FINSEQ_1:def_4;
then reconsider t = F . (len F) as Element of D by A12;
len G >= 1 by A11, NAT_1:14;
then A13: 1 in dom G by FINSEQ_3:25;
consider d being Element of D, f being Function of NAT,D such that
A14: f . 1 = G . 1 and
A15: for n being Element of NAT st 0 <> n & n < len G holds
f . (n + 1) = g . ((f . n),(G . (n + 1))) and
A16: d = f . (len G) by A4, A5, A11, FINSEQ_3:53;
deffunc H1( Element of NAT ) -> Element of D = f . $1;
consider h being Function of NAT,D such that
A17: h . j = g . (d,t) and
A18: for n being Element of NAT st n <> j holds
h . n = H1(n) from FUNCT_2:sch_6();
take a = h . j; ::_thesis: ex h being Function of NAT,D st
( h . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
take h = h; ::_thesis: ( h . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
1 <> j by A5, A11, FINSEQ_3:53;
hence h . 1 = G . 1 by A14, A18
.= F . 1 by A13, FUNCT_1:47 ;
::_thesis: ( ( for n being Element of NAT st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
thus for n being Element of NAT st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ::_thesis: a = h . (len F)
proof
let n be Element of NAT ; ::_thesis: ( 0 <> n & n < len F implies h . (n + 1) = g . ((h . n),(F . (n + 1))) )
assume that
A19: n <> 0 and
A20: n < len F ; ::_thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
now__::_thesis:_h_._(n_+_1)_=_g_._((h_._n),(F_._(n_+_1)))
percases ( n + 1 = len F or n + 1 <> len F ) ;
supposeA21: n + 1 = len F ; ::_thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
len G <> len F by A5, A6;
hence h . (n + 1) = g . ((h . n),(F . (n + 1))) by A5, A6, A16, A17, A18, A21; ::_thesis: verum
end;
supposeA22: n + 1 <> len F ; ::_thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
n + 1 <= len F by A20, NAT_1:13;
then A23: n + 1 < len F by A22, XXREAL_0:1;
then A24: n < len G by A5, A6, XREAL_1:6;
( 1 <= n + 1 & n + 1 <= len G ) by A5, A6, A23, NAT_1:12, NAT_1:13;
then A25: n + 1 in dom G by FINSEQ_3:25;
h . (n + 1) = f . (n + 1) by A18, A22
.= g . ((f . n),(G . (n + 1))) by A15, A19, A24
.= g . ((f . n),(F . (n + 1))) by A25, FUNCT_1:47
.= g . ((h . n),(F . (n + 1))) by A18, A20 ;
hence h . (n + 1) = g . ((h . n),(F . (n + 1))) ; ::_thesis: verum
end;
end;
end;
hence h . (n + 1) = g . ((h . n),(F . (n + 1))) ; ::_thesis: verum
end;
thus a = h . (len F) ; ::_thesis: verum
end;
end;
end;
hence ex d being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) ; ::_thesis: verum
end;
A26: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A26, A3);
hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) by A2; ::_thesis: verum
end;
end;
end;
hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of D holds
( ( g is having_a_unity & len F = 0 & b1 = the_unity_wrt g & b2 = the_unity_wrt g implies b1 = b2 ) & ( ( not g is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b2 = f . (len F) ) implies b1 = b2 ) )
proof
let d1, d2 be Element of D; ::_thesis: ( ( g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 = the_unity_wrt g implies d1 = d2 ) & ( ( not g is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d1 = f . (len F) ) & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d2 = f . (len F) ) implies d1 = d2 ) )
thus ( g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 = the_unity_wrt g implies d1 = d2 ) ; ::_thesis: ( ( not g is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d1 = f . (len F) ) & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d2 = f . (len F) ) implies d1 = d2 )
assume A27: ( not g is having_a_unity or len F <> 0 ) ; ::_thesis: ( for f being Function of NAT,D holds
( not f . 1 = F . 1 or ex n being Element of NAT st
( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d1 = f . (len F) ) or for f being Function of NAT,D holds
( not f . 1 = F . 1 or ex n being Element of NAT st
( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d2 = f . (len F) ) or d1 = d2 )
given f1 being Function of NAT,D such that A28: f1 . 1 = F . 1 and
A29: for n being Element of NAT st 0 <> n & n < len F holds
f1 . (n + 1) = g . ((f1 . n),(F . (n + 1))) and
A30: d1 = f1 . (len F) ; ::_thesis: ( for f being Function of NAT,D holds
( not f . 1 = F . 1 or ex n being Element of NAT st
( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d2 = f . (len F) ) or d1 = d2 )
given f2 being Function of NAT,D such that A31: f2 . 1 = F . 1 and
A32: for n being Element of NAT st 0 <> n & n < len F holds
f2 . (n + 1) = g . ((f2 . n),(F . (n + 1))) and
A33: d2 = f2 . (len F) ; ::_thesis: d1 = d2
defpred S1[ Element of NAT ] means ( $1 <> 0 & $1 <= len F implies f1 . $1 = f2 . $1 );
A34: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A35: ( n <> 0 & n <= len F implies f1 . n = f2 . n ) ; ::_thesis: S1[n + 1]
assume that
n + 1 <> 0 and
A36: n + 1 <= len F ; ::_thesis: f1 . (n + 1) = f2 . (n + 1)
now__::_thesis:_f1_._(n_+_1)_=_f2_._(n_+_1)
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: f1 . (n + 1) = f2 . (n + 1)
hence f1 . (n + 1) = f2 . (n + 1) by A28, A31; ::_thesis: verum
end;
supposeA37: n <> 0 ; ::_thesis: f1 . (n + 1) = f2 . (n + 1)
A38: n < len F by A36, NAT_1:13;
then f1 . (n + 1) = g . ((f1 . n),(F . (n + 1))) by A29, A37;
hence f1 . (n + 1) = f2 . (n + 1) by A32, A35, A37, A38; ::_thesis: verum
end;
end;
end;
hence f1 . (n + 1) = f2 . (n + 1) ; ::_thesis: verum
end;
A39: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A39, A34);
hence d1 = d2 by A1, A27, A30, A33; ::_thesis: verum
end;
consistency
for b1 being Element of D holds verum ;
end;
:: deftheorem Def1 defines "**" FINSOP_1:def_1_:_
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds
for b4 being Element of D holds
( ( g is having_a_unity & len F = 0 implies ( b4 = g "**" F iff b4 = the_unity_wrt g ) ) & ( ( not g is having_a_unity or not len F = 0 ) implies ( b4 = g "**" F iff ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b4 = f . (len F) ) ) ) );
theorem :: FINSOP_1:1
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & g "**" F = f . (len F) ) by Def1;
theorem :: FINSOP_1:2
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st len F >= 1 & ex f being Function of NAT,D st
( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) holds
d = g "**" F by Def1;
definition
let A be non empty set ;
let F be Function of NAT,A;
let p be FinSequence of A;
:: original: +*
redefine funcF +* p -> Function of NAT,A;
coherence
F +* p is Function of NAT,A
proof
A1: dom F = NAT by FUNCT_2:def_1;
dom (F +* p) = (dom F) \/ (dom p) by FUNCT_4:def_1
.= NAT by A1, XBOOLE_1:12 ;
hence F +* p is Function of NAT,A by FUNCT_2:def_1; ::_thesis: verum
end;
end;
notation
let f be FinSequence;
synonym findom f for dom f;
end;
definition
let f be FinSequence;
:: original: findom
redefine func findom f -> Element of Fin NAT;
coherence
findom f is Element of Fin NAT
proof
dom f = Seg (len f) by FINSEQ_1:def_3;
hence findom f is Element of Fin NAT by FINSUB_1:def_5; ::_thesis: verum
end;
end;
Lm1: for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
proof
let D be non empty set ; ::_thesis: for F being FinSequence of D
for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let g be BinOp of D; ::_thesis: ( len F >= 1 & g is associative & g is commutative implies g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) )
assume that
A1: len F >= 1 and
A2: ( g is associative & g is commutative ) ; ::_thesis: g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
set A = findom F;
set h = (NAT --> (the_unity_wrt g)) +* F;
A3: dom F = Seg (len F) by FINSEQ_1:def_3;
then consider G being Function of (Fin NAT),D such that
A4: g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) = G . (findom F) and
for d being Element of D st d is_a_unity_wrt g holds
G . {} = d and
A5: for n being Element of NAT holds G . {n} = ((NAT --> (the_unity_wrt g)) +* F) . n and
A6: for B being Element of Fin NAT st B c= findom F & B <> {} holds
for n being Element of NAT st n in (findom F) \ B holds
G . (B \/ {n}) = g . ((G . B),(((NAT --> (the_unity_wrt g)) +* F) . n)) by A1, A2, SETWISEO:def_3;
consider f being Function of NAT,D such that
A7: f . 1 = F . 1 and
A8: for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) and
A9: g "**" F = f . (len F) by A1, Def1;
defpred S1[ Element of NAT ] means ( $1 <> 0 & $1 <= len F implies f . $1 = G . (Seg $1) );
A10: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A11: ( n <> 0 & n <= len F implies f . n = G . (Seg n) ) ; ::_thesis: S1[n + 1]
assume that
n + 1 <> 0 and
A12: n + 1 <= len F ; ::_thesis: f . (n + 1) = G . (Seg (n + 1))
now__::_thesis:_f_._(n_+_1)_=_G_._(Seg_(n_+_1))
percases ( n = 0 or n <> 0 ) ;
supposeA13: n = 0 ; ::_thesis: f . (n + 1) = G . (Seg (n + 1))
1 in dom F by A1, A3, FINSEQ_1:1;
then ((NAT --> (the_unity_wrt g)) +* F) . 1 = F . 1 by FUNCT_4:13;
hence f . (n + 1) = G . (Seg (n + 1)) by A7, A5, A13, FINSEQ_1:2; ::_thesis: verum
end;
supposeA14: n <> 0 ; ::_thesis: f . (n + 1) = G . (Seg (n + 1))
reconsider B = Seg n as Element of Fin NAT by FINSUB_1:def_5;
n + 1 >= 1 by NAT_1:12;
then A15: n + 1 in dom F by A12, FINSEQ_3:25;
A16: n < len F by A12, NAT_1:13;
then A17: f . (n + 1) = g . ((f . n),(F . (n + 1))) by A8, A14;
not n + 1 in Seg n by FINSEQ_3:10;
then A18: n + 1 in (findom F) \ (Seg n) by A15, XBOOLE_0:def_5;
A19: Seg n c= findom F by A3, A16, FINSEQ_1:5;
G . (Seg (n + 1)) = G . ((Seg n) \/ {(n + 1)}) by FINSEQ_1:9
.= g . ((G . B),(((NAT --> (the_unity_wrt g)) +* F) . (n + 1))) by A6, A14, A19, A18 ;
hence f . (n + 1) = G . (Seg (n + 1)) by A11, A12, A14, A17, A15, FUNCT_4:13, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence f . (n + 1) = G . (Seg (n + 1)) ; ::_thesis: verum
end;
A20: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A10);
hence g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) by A1, A9, A3, A4; ::_thesis: verum
end;
Lm2: for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
proof
let D be non empty set ; ::_thesis: for F being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let g be BinOp of D; ::_thesis: ( len F = 0 & g is having_a_unity & g is associative & g is commutative implies g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) )
assume that
A1: len F = 0 and
A2: g is having_a_unity and
A3: ( g is associative & g is commutative ) ; ::_thesis: g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
F = {} by A1;
then A4: dom F = {}. NAT ;
thus g "**" F = the_unity_wrt g by A1, A2, Def1
.= g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) by A2, A3, A4, SETWISEO:31 ; ::_thesis: verum
end;
theorem :: FINSOP_1:3
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
proof
let D be non empty set ; ::_thesis: for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let F be FinSequence of D; ::_thesis: for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let g be BinOp of D; ::_thesis: ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative implies g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) )
( len F = 0 or len F >= 1 ) by NAT_1:14;
hence ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative implies g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) ) by Lm1, Lm2; ::_thesis: verum
end;
Lm3: for D being non empty set
for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g
proof
let D be non empty set ; ::_thesis: for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g
let g be BinOp of D; ::_thesis: ( g is having_a_unity implies g "**" (<*> D) = the_unity_wrt g )
A1: len (<*> D) = 0 ;
assume g is having_a_unity ; ::_thesis: g "**" (<*> D) = the_unity_wrt g
hence g "**" (<*> D) = the_unity_wrt g by A1, Def1; ::_thesis: verum
end;
Lm4: for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d
proof
let D be non empty set ; ::_thesis: for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d
let d be Element of D; ::_thesis: for g being BinOp of D holds g "**" <*d*> = d
let g be BinOp of D; ::_thesis: g "**" <*d*> = d
A1: len <*d*> = 1 by FINSEQ_1:39;
then ex f being Function of NAT,D st
( f . 1 = <*d*> . 1 & ( for n being Element of NAT st 0 <> n & n < len <*d*> holds
f . (n + 1) = g . ((f . n),(<*d*> . (n + 1))) ) & g "**" <*d*> = f . (len <*d*>) ) by Def1;
hence g "**" <*d*> = d by A1, FINSEQ_1:def_8; ::_thesis: verum
end;
Lm5: for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let d be Element of D; ::_thesis: for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let g be BinOp of D; ::_thesis: ( len F >= 1 implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) )
set G = F ^ <*d*>;
A1: (F ^ <*d*>) . ((len F) + 1) = d by FINSEQ_1:42;
A2: len (F ^ <*d*>) = (len F) + (len <*d*>) by FINSEQ_1:22
.= (len F) + 1 by FINSEQ_1:39 ;
then 1 <= len (F ^ <*d*>) by NAT_1:12;
then consider f1 being Function of NAT,D such that
A3: f1 . 1 = (F ^ <*d*>) . 1 and
A4: for n being Element of NAT st 0 <> n & n < len (F ^ <*d*>) holds
f1 . (n + 1) = g . ((f1 . n),((F ^ <*d*>) . (n + 1))) and
A5: g "**" (F ^ <*d*>) = f1 . (len (F ^ <*d*>)) by Def1;
assume A6: len F >= 1 ; ::_thesis: g "**" (F ^ <*d*>) = g . ((g "**" F),d)
then consider f being Function of NAT,D such that
A7: f . 1 = F . 1 and
A8: for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) and
A9: g "**" F = f . (len F) by Def1;
defpred S1[ Element of NAT ] means ( 0 <> $1 & $1 < len (F ^ <*d*>) implies f . $1 = f1 . $1 );
A10: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A11: S1[n] ; ::_thesis: S1[n + 1]
assume that
A12: 0 <> n + 1 and
A13: n + 1 < len (F ^ <*d*>) ; ::_thesis: f . (n + 1) = f1 . (n + 1)
A14: n + 1 >= 1 by A12, NAT_1:14;
now__::_thesis:_f_._(n_+_1)_=_f1_._(n_+_1)
percases ( n + 1 = 1 or n + 1 > 1 ) by A14, XXREAL_0:1;
supposeA15: n + 1 = 1 ; ::_thesis: f . (n + 1) = f1 . (n + 1)
1 in dom F by A6, FINSEQ_3:25;
hence f . (n + 1) = f1 . (n + 1) by A7, A3, A15, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA16: n + 1 > 1 ; ::_thesis: f . (n + 1) = f1 . (n + 1)
then n <> 0 ;
then A17: f1 . (n + 1) = g . ((f1 . n),((F ^ <*d*>) . (n + 1))) by A4, A13, NAT_1:12;
A18: n + 1 <= len F by A2, A13, NAT_1:13;
then A19: n < len F by NAT_1:13;
1 <= n + 1 by NAT_1:12;
then A20: n + 1 in dom F by A18, FINSEQ_3:25;
n + 1 > 0 + 1 by A16;
then f . (n + 1) = g . ((f . n),(F . (n + 1))) by A8, A19;
hence f . (n + 1) = f1 . (n + 1) by A11, A13, A16, A17, A20, FINSEQ_1:def_7, NAT_1:12; ::_thesis: verum
end;
end;
end;
hence f . (n + 1) = f1 . (n + 1) ; ::_thesis: verum
end;
A21: S1[ 0 ] ;
A22: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A10);
g "**" (F ^ <*d*>) = g . ((f1 . (len F)),((F ^ <*d*>) . ((len F) + 1))) by A6, A2, A4, A5, XREAL_1:29;
hence g "**" (F ^ <*d*>) = g . ((g "**" F),d) by A6, A9, A2, A1, A22, XREAL_1:29; ::_thesis: verum
end;
Lm6: for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let d be Element of D; ::_thesis: for F being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let g be BinOp of D; ::_thesis: ( g is having_a_unity & len F = 0 implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) )
assume that
A1: g is having_a_unity and
A2: len F = 0 ; ::_thesis: g "**" (F ^ <*d*>) = g . ((g "**" F),d)
F = <*> D by A2;
hence g "**" (F ^ <*d*>) = g "**" <*d*> by FINSEQ_1:34
.= d by Lm4
.= g . ((the_unity_wrt g),d) by A1, SETWISEO:15
.= g . ((g "**" F),d) by A1, A2, Def1 ;
::_thesis: verum
end;
theorem Th4: :: FINSOP_1:4
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let d be Element of D; ::_thesis: for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let F be FinSequence of D; ::_thesis: for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let g be BinOp of D; ::_thesis: ( ( g is having_a_unity or len F >= 1 ) implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) )
( len F >= 1 or len F = 0 ) by NAT_1:14;
hence ( ( g is having_a_unity or len F >= 1 ) implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) ) by Lm5, Lm6; ::_thesis: verum
end;
theorem Th5: :: FINSOP_1:5
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
g "**" (F ^ G) = g . ((g "**" F),(g "**" G))
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
g "**" (F ^ G) = g . ((g "**" F),(g "**" G))
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
g "**" (F ^ G) = g . ((g "**" F),(g "**" G))
let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) )
defpred S1[ FinSequence of D] means for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds
g "**" (F ^ $1) = g . ((g "**" F),(g "**" $1));
A1: for G being FinSequence of D
for d being Element of D st S1[G] holds
S1[G ^ <*d*>]
proof
let G be FinSequence of D; ::_thesis: for d being Element of D st S1[G] holds
S1[G ^ <*d*>]
let d be Element of D; ::_thesis: ( S1[G] implies S1[G ^ <*d*>] )
assume A2: S1[G] ; ::_thesis: S1[G ^ <*d*>]
let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) holds
g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>)))
let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) implies g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) )
assume that
A3: g is associative and
A4: ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) ; ::_thesis: g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>)))
A5: now__::_thesis:_(_not_g_is_having_a_unity_implies_len_(F_^_G)_>=_1_)
A6: len (F ^ G) = (len F) + (len G) by FINSEQ_1:22;
assume not g is having_a_unity ; ::_thesis: len (F ^ G) >= 1
hence len (F ^ G) >= 1 by A4, A6, NAT_1:12; ::_thesis: verum
end;
A7: g "**" (F ^ (G ^ <*d*>)) = g "**" ((F ^ G) ^ <*d*>) by FINSEQ_1:32
.= g . ((g "**" (F ^ G)),d) by A5, Th4 ;
now__::_thesis:_g_"**"_(F_^_(G_^_<*d*>))_=_g_._((g_"**"_F),(g_"**"_(G_^_<*d*>)))
percases ( len G <> 0 or len G = 0 ) ;
supposeA8: len G <> 0 ; ::_thesis: g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>)))
then len G >= 1 by NAT_1:14;
hence g "**" (F ^ (G ^ <*d*>)) = g . ((g . ((g "**" F),(g "**" G))),d) by A2, A3, A4, A7
.= g . ((g "**" F),(g . ((g "**" G),d))) by A3, BINOP_1:def_3
.= g . ((g "**" F),(g "**" (G ^ <*d*>))) by A8, Th4, NAT_1:14 ;
::_thesis: verum
end;
suppose len G = 0 ; ::_thesis: g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>)))
then A9: G = {} ;
hence g "**" (F ^ (G ^ <*d*>)) = g "**" (F ^ <*d*>) by FINSEQ_1:34
.= g . ((g "**" F),d) by A4, Th4
.= g . ((g "**" F),(g "**" <*d*>)) by Lm4
.= g . ((g "**" F),(g "**" (G ^ <*d*>))) by A9, FINSEQ_1:34 ;
::_thesis: verum
end;
end;
end;
hence g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>))) ; ::_thesis: verum
end;
A10: S1[ <*> D]
proof
let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) holds
g "**" (F ^ (<*> D)) = g . ((g "**" F),(g "**" (<*> D)))
let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) implies g "**" (F ^ (<*> D)) = g . ((g "**" F),(g "**" (<*> D))) )
assume that
g is associative and
A11: ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) ; ::_thesis: g "**" (F ^ (<*> D)) = g . ((g "**" F),(g "**" (<*> D)))
thus g "**" (F ^ (<*> D)) = g "**" F by FINSEQ_1:34
.= g . ((g "**" F),(the_unity_wrt g)) by A11, SETWISEO:15
.= g . ((g "**" F),(g "**" (<*> D))) by A11, Lm3 ; ::_thesis: verum
end;
for G being FinSequence of D holds S1[G] from FINSEQ_2:sch_2(A10, A1);
hence ( g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies g "**" (F ^ G) = g . ((g "**" F),(g "**" G)) ) ; ::_thesis: verum
end;
theorem Th6: :: FINSOP_1:6
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
let d be Element of D; ::_thesis: for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
let F be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
let g be BinOp of D; ::_thesis: ( g is associative & ( g is having_a_unity or len F >= 1 ) implies g "**" (<*d*> ^ F) = g . (d,(g "**" F)) )
A1: len <*d*> = 1 by FINSEQ_1:39;
assume ( g is associative & ( g is having_a_unity or len F >= 1 ) ) ; ::_thesis: g "**" (<*d*> ^ F) = g . (d,(g "**" F))
hence g "**" (<*d*> ^ F) = g . ((g "**" <*d*>),(g "**" F)) by A1, Th5
.= g . (d,(g "**" F)) by Lm4 ;
::_thesis: verum
end;
Lm7: for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
let g be BinOp of D; ::_thesis: ( g is associative & g is commutative implies for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G )
assume that
A1: g is associative and
A2: g is commutative ; ::_thesis: for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
defpred S1[ Element of NAT ] means for H1, H2 being FinSequence of D st len H1 >= 1 & len H1 = $1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2;
A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let H1, H2 be FinSequence of D; ::_thesis: ( len H1 >= 1 & len H1 = k + 1 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2 )
assume that
len H1 >= 1 and
A5: len H1 = k + 1 and
A6: len H1 = len H2 ; ::_thesis: for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2
reconsider p = H2 | (Seg k) as FinSequence of D by FINSEQ_1:18;
let f be Permutation of (dom H1); ::_thesis: ( ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) implies g "**" H1 = g "**" H2 )
A7: dom H1 = Seg (k + 1) by A5, FINSEQ_1:def_3;
then A8: rng f = Seg (k + 1) by FUNCT_2:def_3;
A9: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_holds_
f_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: ( n in dom f implies f . n is Element of NAT )
assume n in dom f ; ::_thesis: f . n is Element of NAT
then f . n in Seg (k + 1) by A8, FUNCT_1:def_3;
hence f . n is Element of NAT ; ::_thesis: verum
end;
A10: rng H2 c= D by FINSEQ_1:def_4;
( Seg (k + 1) = {} implies Seg (k + 1) = {} ) ;
then A11: dom f = Seg (k + 1) by A7, FUNCT_2:def_1;
A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A13: f . (k + 1) in Seg (k + 1) by A11, A8, FUNCT_1:def_3;
then reconsider n = f . (k + 1) as Element of NAT ;
A14: dom H2 = Seg (k + 1) by A5, A6, FINSEQ_1:def_3;
then H2 . (k + 1) in rng H2 by A12, FUNCT_1:def_3;
then reconsider d = H2 . (k + 1) as Element of D by A10;
A15: n <= k + 1 by A13, FINSEQ_1:1;
then consider m2 being Nat such that
A16: n + m2 = k + 1 by NAT_1:10;
defpred S2[ Nat, set ] means $2 = H1 . (n + $1);
1 <= n by A13, FINSEQ_1:1;
then consider m1 being Nat such that
A17: 1 + m1 = n by NAT_1:10;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def_12;
A18: for j being Nat st j in Seg m2 holds
ex x being set st S2[j,x] ;
consider q2 being FinSequence such that
A19: dom q2 = Seg m2 and
A20: for k being Nat st k in Seg m2 holds
S2[k,q2 . k] from FINSEQ_1:sch_1(A18);
rng q2 c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q2 or x in D )
assume x in rng q2 ; ::_thesis: x in D
then consider y being set such that
A21: y in findom q2 and
A22: x = q2 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A21, SETWISEO:9;
1 <= y by A19, A21, FINSEQ_1:1;
then A23: 1 <= n + y by NAT_1:12;
y <= m2 by A19, A21, FINSEQ_1:1;
then n + y <= len H1 by A5, A16, XREAL_1:7;
then n + y in Seg (len H1) by A23, FINSEQ_1:1;
then n + y in dom H1 by FINSEQ_1:def_3;
then A24: H1 . (n + y) in rng H1 by FUNCT_1:def_3;
rng H1 c= D by FINSEQ_1:def_4;
then reconsider xx = H1 . (n + y) as Element of D by A24;
xx in D ;
hence x in D by A19, A20, A21, A22; ::_thesis: verum
end;
then reconsider q2 = q2 as FinSequence of D by FINSEQ_1:def_4;
reconsider q1 = H1 | (Seg m1) as FinSequence of D by FINSEQ_1:18;
defpred S3[ Nat, set ] means ( ( f . $1 in dom q1 implies $2 = f . $1 ) & ( not f . $1 in dom q1 implies for l being Element of NAT st l = f . $1 holds
$2 = l - 1 ) );
A25: k <= k + 1 by NAT_1:12;
then A26: Seg k c= Seg (k + 1) by FINSEQ_1:5;
A27: for i being Nat st i in Seg k holds
ex y being set st S3[i,y]
proof
let i be Nat; ::_thesis: ( i in Seg k implies ex y being set st S3[i,y] )
assume A28: i in Seg k ; ::_thesis: ex y being set st S3[i,y]
now__::_thesis:_(_not_f_._i_in_dom_q1_implies_ex_y_being_set_st_
(_(_f_._i_in_dom_q1_implies_y_=_f_._i_)_&_(_not_f_._i_in_dom_q1_implies_for_t_being_Element_of_NAT_st_t_=_f_._i_holds_
y_=_t_-_1_)_)_)
f . i in Seg (k + 1) by A11, A8, A26, A28, FUNCT_1:def_3;
then reconsider j = f . i as Element of NAT ;
assume A29: not f . i in dom q1 ; ::_thesis: ex y being set st
( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds
y = t - 1 ) )
take y = j - 1; ::_thesis: ( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds
y = t - 1 ) )
thus ( f . i in dom q1 implies y = f . i ) by A29; ::_thesis: ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds
y = t - 1 )
assume not f . i in dom q1 ; ::_thesis: for t being Element of NAT st t = f . i holds
y = t - 1
let t be Element of NAT ; ::_thesis: ( t = f . i implies y = t - 1 )
assume t = f . i ; ::_thesis: y = t - 1
hence y = t - 1 ; ::_thesis: verum
end;
hence ex y being set st S3[i,y] ; ::_thesis: verum
end;
consider gg being FinSequence such that
A30: dom gg = Seg k and
A31: for i being Nat st i in Seg k holds
S3[i,gg . i] from FINSEQ_1:sch_1(A27);
A32: dom p = Seg k by A5, A6, A25, FINSEQ_1:17;
m1 <= n by A17, NAT_1:11;
then A33: m1 <= k + 1 by A15, XXREAL_0:2;
then A34: dom q1 = Seg m1 by A5, FINSEQ_1:17;
A35: now__::_thesis:_for_i,_l_being_Element_of_NAT_st_l_=_f_._i_&_not_f_._i_in_dom_q1_&_i_in_dom_gg_holds_
m1_+_2_<=_l
let i, l be Element of NAT ; ::_thesis: ( l = f . i & not f . i in dom q1 & i in dom gg implies m1 + 2 <= l )
assume that
A36: l = f . i and
A37: not f . i in dom q1 and
A38: i in dom gg ; ::_thesis: m1 + 2 <= l
A39: ( l < 1 or m1 < l ) by A34, A36, A37, FINSEQ_1:1;
A40: now__::_thesis:_not_m1_+_1_=_l
assume m1 + 1 = l ; ::_thesis: contradiction
then k + 1 = i by A12, A11, A17, A26, A30, A36, A38, FUNCT_1:def_4;
then k + 1 <= k + 0 by A30, A38, FINSEQ_1:1;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
f . i in rng f by A11, A26, A30, A38, FUNCT_1:def_3;
then m1 + 1 <= l by A8, A36, A39, FINSEQ_1:1, NAT_1:13;
then m1 + 1 < l by A40, XXREAL_0:1;
then (m1 + 1) + 1 <= l by NAT_1:13;
hence m1 + 2 <= l ; ::_thesis: verum
end;
1 + k = 1 + (m1 + m2) by A17, A16;
then A41: m1 <= k by NAT_1:11;
A42: rng gg c= dom p
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng gg or y in dom p )
assume y in rng gg ; ::_thesis: y in dom p
then consider x being set such that
A43: x in findom gg and
A44: gg . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A43, SETWISEO:9;
now__::_thesis:_y_in_dom_p
percases ( f . x in dom q1 or not f . x in dom q1 ) ;
supposeA45: f . x in dom q1 ; ::_thesis: y in dom p
A46: dom q1 c= dom p by A41, A34, A32, FINSEQ_1:5;
f . x = gg . x by A30, A31, A43, A45;
hence y in dom p by A44, A45, A46; ::_thesis: verum
end;
supposeA47: not f . x in dom q1 ; ::_thesis: y in dom p
reconsider j = f . x as Element of NAT by A11, A26, A9, A30, A43;
A48: f . x in Seg (k + 1) by A11, A8, A26, A30, A43, FUNCT_1:def_3;
( j < 1 or m1 < j ) by A34, A47, FINSEQ_1:1;
then reconsider l = j - 1 as Element of NAT by A48, FINSEQ_1:1, NAT_1:20;
j <= k + 1 by A48, FINSEQ_1:1;
then A49: l <= (k + 1) - 1 by XREAL_1:9;
m1 + 2 <= j by A35, A43, A47;
then A50: (m1 + 2) - 1 <= l by XREAL_1:9;
1 <= m1 + 1 by NAT_1:12;
then A51: 1 <= l by A50, XXREAL_0:2;
gg . x = j - 1 by A30, A31, A43, A47;
hence y in dom p by A32, A44, A51, A49, FINSEQ_1:1; ::_thesis: verum
end;
end;
end;
hence y in dom p ; ::_thesis: verum
end;
A52: len q1 = m1 by A5, A33, FINSEQ_1:17;
A53: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q2_holds_
H1_._((len_(q1_^_<*d*>))_+_j)_=_q2_._j
let j be Nat; ::_thesis: ( j in dom q2 implies H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j )
assume A54: j in dom q2 ; ::_thesis: H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j
len (q1 ^ <*d*>) = m1 + (len <*d*>) by A52, FINSEQ_1:22
.= n by A17, FINSEQ_1:39 ;
hence H1 . ((len (q1 ^ <*d*>)) + j) = q2 . j by A19, A20, A54; ::_thesis: verum
end;
set q = q1 ^ q2;
A55: len q2 = m2 by A19, FINSEQ_1:def_3;
then A56: len (q1 ^ q2) = m1 + m2 by A52, FINSEQ_1:22;
then A57: dom (q1 ^ q2) = Seg k by A17, A16, FINSEQ_1:def_3;
then reconsider gg = gg as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A32, A30, A42, FUNCT_2:2;
A58: len p = k by A5, A6, A25, FINSEQ_1:17;
A59: rng gg = dom (q1 ^ q2)
proof
thus rng gg c= dom (q1 ^ q2) by A17, A16, A56, A32, A42, FINSEQ_1:def_3; :: according to XBOOLE_0:def_10 ::_thesis: dom (q1 ^ q2) c= rng gg
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (q1 ^ q2) or y in rng gg )
assume A60: y in dom (q1 ^ q2) ; ::_thesis: y in rng gg
then reconsider j = y as Element of NAT ;
consider x being set such that
A61: x in dom f and
A62: f . x = y by A8, A26, A57, A60, FUNCT_1:def_3;
reconsider x = x as Element of NAT by A11, A61;
now__::_thesis:_y_in_rng_gg
percases ( x in dom gg or not x in dom gg ) ;
supposeA63: x in dom gg ; ::_thesis: y in rng gg
now__::_thesis:_y_in_rng_gg
percases ( f . x in dom q1 or not f . x in dom q1 ) ;
suppose f . x in dom q1 ; ::_thesis: y in rng gg
then gg . x = f . x by A30, A31, A63;
hence y in rng gg by A62, A63, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA64: not f . x in dom q1 ; ::_thesis: y in rng gg
j <= k by A57, A60, FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7;
then j + 1 in rng f by A8, FINSEQ_1:1;
then consider x1 being set such that
A65: x1 in dom f and
A66: f . x1 = j + 1 by FUNCT_1:def_3;
A67: now__::_thesis:_x1_in_dom_gg
assume not x1 in dom gg ; ::_thesis: contradiction
then x1 in (Seg (k + 1)) \ (Seg k) by A7, A30, A65, XBOOLE_0:def_5;
then x1 in {(k + 1)} by FINSEQ_3:15;
then A68: j + 1 = m1 + 1 by A17, A66, TARSKI:def_1;
1 <= j by A57, A60, FINSEQ_1:1;
hence contradiction by A34, A62, A64, A68, FINSEQ_1:1; ::_thesis: verum
end;
( j < 1 or m1 < j ) by A34, A62, A64, FINSEQ_1:1;
then not j + 1 <= m1 by A57, A60, FINSEQ_1:1, NAT_1:13;
then not f . x1 in dom q1 by A34, A66, FINSEQ_1:1;
then gg . x1 = (j + 1) - 1 by A30, A31, A66, A67
.= y ;
hence y in rng gg by A67, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence y in rng gg ; ::_thesis: verum
end;
supposeA69: not x in dom gg ; ::_thesis: y in rng gg
j <= k by A57, A60, FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7;
then j + 1 in rng f by A8, FINSEQ_1:1;
then consider x1 being set such that
A70: x1 in dom f and
A71: f . x1 = j + 1 by FUNCT_1:def_3;
x in (Seg (k + 1)) \ (Seg k) by A7, A30, A61, A69, XBOOLE_0:def_5;
then x in {(k + 1)} by FINSEQ_3:15;
then A72: x = k + 1 by TARSKI:def_1;
A73: now__::_thesis:_x1_in_dom_gg
assume not x1 in dom gg ; ::_thesis: contradiction
then x1 in (Seg (k + 1)) \ (Seg k) by A7, A30, A70, XBOOLE_0:def_5;
then x1 in {(k + 1)} by FINSEQ_3:15;
then j + 1 = j + 0 by A62, A72, A71, TARSKI:def_1;
hence contradiction ; ::_thesis: verum
end;
m1 <= j by A17, A62, A72, XREAL_1:29;
then not j + 1 <= m1 by NAT_1:13;
then not f . x1 in dom q1 by A34, A71, FINSEQ_1:1;
then gg . x1 = (j + 1) - 1 by A30, A31, A71, A73
.= y ;
hence y in rng gg by A73, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence y in rng gg ; ::_thesis: verum
end;
assume A74: for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ; ::_thesis: g "**" H1 = g "**" H2
then A75: H2 . (k + 1) = H1 . (f . (k + 1)) by A14, FINSEQ_1:4;
A76: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(q1_^_<*d*>)_holds_
H1_._j_=_(q1_^_<*d*>)_._j
let j be Nat; ::_thesis: ( j in dom (q1 ^ <*d*>) implies H1 . j = (q1 ^ <*d*>) . j )
assume A77: j in dom (q1 ^ <*d*>) ; ::_thesis: H1 . j = (q1 ^ <*d*>) . j
A78: now__::_thesis:_(_j_in_Seg_m1_implies_H1_._j_=_(q1_^_<*d*>)_._j_)
assume j in Seg m1 ; ::_thesis: H1 . j = (q1 ^ <*d*>) . j
then A79: j in dom q1 by A5, A33, FINSEQ_1:17;
then q1 . j = H1 . j by FUNCT_1:47;
hence H1 . j = (q1 ^ <*d*>) . j by A79, FINSEQ_1:def_7; ::_thesis: verum
end;
A80: now__::_thesis:_(_j_in_{n}_implies_(q1_^_<*d*>)_._j_=_H1_._j_)
( 1 in Seg 1 & len <*d*> = 1 ) by FINSEQ_1:1, FINSEQ_1:39;
then 1 in dom <*d*> by FINSEQ_1:def_3;
then A81: (q1 ^ <*d*>) . ((len q1) + 1) = <*d*> . 1 by FINSEQ_1:def_7;
assume j in {n} ; ::_thesis: (q1 ^ <*d*>) . j = H1 . j
then j = n by TARSKI:def_1;
hence (q1 ^ <*d*>) . j = H1 . j by A75, A17, A52, A81, FINSEQ_1:40; ::_thesis: verum
end;
len (q1 ^ <*d*>) = m1 + (len <*d*>) by A52, FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40 ;
then j in Seg (m1 + 1) by A77, FINSEQ_1:def_3;
then j in (Seg m1) \/ {n} by A17, FINSEQ_1:9;
hence H1 . j = (q1 ^ <*d*>) . j by A78, A80, XBOOLE_0:def_3; ::_thesis: verum
end;
gg is one-to-one
proof
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y1 in findom gg or not b1 in findom gg or not gg . y1 = gg . b1 or y1 = b1 )
let y2 be set ; ::_thesis: ( not y1 in findom gg or not y2 in findom gg or not gg . y1 = gg . y2 or y1 = y2 )
assume that
A82: y1 in dom gg and
A83: y2 in dom gg and
A84: gg . y1 = gg . y2 ; ::_thesis: y1 = y2
reconsider j1 = y1, j2 = y2 as Element of NAT by A30, A82, A83;
A85: f . y2 in Seg (k + 1) by A11, A8, A26, A30, A83, FUNCT_1:def_3;
A86: f . y1 in Seg (k + 1) by A11, A8, A26, A30, A82, FUNCT_1:def_3;
then reconsider a = f . y1, b = f . y2 as Element of NAT by A85;
now__::_thesis:_y1_=_y2
percases ( ( f . y1 in dom q1 & f . y2 in dom q1 ) or ( f . y1 in dom q1 & not f . y2 in dom q1 ) or ( not f . y1 in dom q1 & f . y2 in dom q1 ) or ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ) ;
suppose ( f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then ( gg . j1 = f . y1 & gg . j2 = f . y2 ) by A30, A31, A82, A83;
hence y1 = y2 by A11, A26, A30, A82, A83, A84, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA87: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then A88: a <= m1 by A34, FINSEQ_1:1;
( gg . j1 = a & gg . j2 = b - 1 ) by A30, A31, A82, A83, A87;
then A89: (b - 1) + 1 <= m1 + 1 by A84, A88, XREAL_1:6;
1 <= b by A85, FINSEQ_1:1;
then A90: b in Seg (m1 + 1) by A89, FINSEQ_1:1;
not b in Seg m1 by A5, A33, A87, FINSEQ_1:17;
then b in (Seg (m1 + 1)) \ (Seg m1) by A90, XBOOLE_0:def_5;
then b in {(m1 + 1)} by FINSEQ_3:15;
then b = m1 + 1 by TARSKI:def_1;
then y2 = k + 1 by A12, A11, A17, A26, A30, A83, FUNCT_1:def_4;
hence y1 = y2 by A30, A83, FINSEQ_3:8; ::_thesis: verum
end;
supposeA91: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then A92: b <= m1 by A34, FINSEQ_1:1;
( gg . j1 = a - 1 & gg . j2 = b ) by A30, A31, A82, A83, A91;
then A93: (a - 1) + 1 <= m1 + 1 by A84, A92, XREAL_1:6;
1 <= a by A86, FINSEQ_1:1;
then A94: a in Seg (m1 + 1) by A93, FINSEQ_1:1;
not a in Seg m1 by A5, A33, A91, FINSEQ_1:17;
then a in (Seg (m1 + 1)) \ (Seg m1) by A94, XBOOLE_0:def_5;
then a in {(m1 + 1)} by FINSEQ_3:15;
then a = m1 + 1 by TARSKI:def_1;
then y1 = k + 1 by A12, A11, A17, A26, A30, A82, FUNCT_1:def_4;
hence y1 = y2 by A30, A82, FINSEQ_3:8; ::_thesis: verum
end;
supposeA95: ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2
then gg . j2 = b - 1 by A30, A31, A83;
then A96: gg . y2 = b + (- 1) ;
gg . j1 = a - 1 by A30, A31, A82, A95;
then gg . j1 = a + (- 1) ;
then a = b by A84, A96, XCMPLX_1:2;
hence y1 = y2 by A11, A26, A30, A82, A83, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence y1 = y2 ; ::_thesis: verum
end;
then reconsider gg = gg as Permutation of (dom (q1 ^ q2)) by A59, FUNCT_2:57;
(len (q1 ^ <*d*>)) + (len q2) = ((len q1) + (len <*d*>)) + m2 by A55, FINSEQ_1:22
.= k + 1 by A17, A16, A52, FINSEQ_1:40 ;
then dom H1 = Seg ((len (q1 ^ <*d*>)) + (len q2)) by A5, FINSEQ_1:def_3;
then A97: H1 = (q1 ^ <*d*>) ^ q2 by A76, A53, FINSEQ_1:def_7;
A98: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_p_holds_
p_._i_=_(q1_^_q2)_._(gg_._i)
let i be Element of NAT ; ::_thesis: ( i in dom p implies p . i = (q1 ^ q2) . (gg . i) )
assume A99: i in dom p ; ::_thesis: p . i = (q1 ^ q2) . (gg . i)
then f . i in rng f by A11, A26, A32, FUNCT_1:def_3;
then reconsider j = f . i as Element of NAT by A8;
now__::_thesis:_p_._i_=_(q1_^_q2)_._(gg_._i)
percases ( f . i in dom q1 or not f . i in dom q1 ) ;
supposeA100: f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (gg . i)
then A101: ( f . i = gg . i & H1 . j = q1 . j ) by A32, A31, A99, FUNCT_1:47;
( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A74, A14, A26, A32, A99, FUNCT_1:47;
hence p . i = (q1 ^ q2) . (gg . i) by A100, A101, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA102: not f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (gg . i)
then m1 + 2 <= j by A32, A30, A35, A99;
then A103: (m1 + 2) - 1 <= j - 1 by XREAL_1:9;
m1 < m1 + 1 by XREAL_1:29;
then A104: m1 < j - 1 by A103, XXREAL_0:2;
then m1 < j by XREAL_1:146, XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
A105: not j1 in dom q1 by A34, A104, FINSEQ_1:1;
A106: gg . i = j - 1 by A32, A31, A99, A102;
then j - 1 in dom (q1 ^ q2) by A32, A30, A59, A99, FUNCT_1:def_3;
then consider a being Nat such that
A107: a in dom q2 and
A108: j1 = (len q1) + a by A105, FINSEQ_1:25;
A109: len <*d*> = 1 by FINSEQ_1:39;
A110: ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A74, A14, A26, A32, A99, FUNCT_1:47;
A111: H1 = q1 ^ (<*d*> ^ q2) by A97, FINSEQ_1:32;
j in dom H1 by A7, A11, A8, A26, A32, A99, FUNCT_1:def_3;
then consider b being Nat such that
A112: b in dom (<*d*> ^ q2) and
A113: j = (len q1) + b by A102, A111, FINSEQ_1:25;
A114: H1 . j = (<*d*> ^ q2) . b by A111, A112, A113, FINSEQ_1:def_7;
A115: b = 1 + a by A108, A113;
(q1 ^ q2) . (j - 1) = q2 . a by A107, A108, FINSEQ_1:def_7;
hence p . i = (q1 ^ q2) . (gg . i) by A106, A110, A107, A114, A115, A109, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence p . i = (q1 ^ q2) . (gg . i) ; ::_thesis: verum
end;
now__::_thesis:_g_"**"_H1_=_g_"**"_H2
percases ( len p <> 0 or len p = 0 ) ;
supposeA116: len p <> 0 ; ::_thesis: g "**" H1 = g "**" H2
A117: H2 = p ^ <*d*> by A5, A6, FINSEQ_3:55;
g "**" p = g "**" (q1 ^ q2) by A4, A17, A16, A58, A56, A98, A116, NAT_1:14;
then A118: g "**" H2 = g . ((g "**" (q1 ^ q2)),d) by A116, A117, Th4, NAT_1:14;
now__::_thesis:_g_"**"_H1_=_g_"**"_H2
percases ( ( len q1 <> 0 & len q2 <> 0 ) or ( len q1 = 0 & len q2 <> 0 ) or ( len q1 <> 0 & len q2 = 0 ) or ( len q1 = 0 & len q2 = 0 ) ) ;
supposeA119: ( len q1 <> 0 & len q2 <> 0 ) ; ::_thesis: g "**" H1 = g "**" H2
( len (<*d*> ^ q2) = (len <*d*>) + (len q2) & len <*d*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
then A120: len (<*d*> ^ q2) >= 1 by NAT_1:12;
A121: len q1 >= 1 by A119, NAT_1:14;
len q2 >= 1 by A119, NAT_1:14;
then g "**" H2 = g . ((g . ((g "**" q1),(g "**" q2))),d) by A1, A118, A121, Th5
.= g . ((g "**" q1),(g . ((g "**" q2),d))) by A1, BINOP_1:def_3
.= g . ((g "**" q1),(g . (d,(g "**" q2)))) by A2, BINOP_1:def_2
.= g . ((g "**" q1),(g "**" (<*d*> ^ q2))) by A1, A119, Th6, NAT_1:14
.= g "**" (q1 ^ (<*d*> ^ q2)) by A1, A121, A120, Th5
.= g "**" H1 by A97, FINSEQ_1:32 ;
hence g "**" H1 = g "**" H2 ; ::_thesis: verum
end;
suppose ( len q1 = 0 & len q2 <> 0 ) ; ::_thesis: g "**" H1 = g "**" H2
then A122: q1 = {} ;
then A123: H1 = <*d*> ^ q2 by A97, FINSEQ_1:34
.= <*d*> ^ (q1 ^ q2) by A122, FINSEQ_1:34 ;
g "**" H2 = g . (d,(g "**" (q1 ^ q2))) by A2, A118, BINOP_1:def_2
.= g "**" (<*d*> ^ (q1 ^ q2)) by A1, A17, A16, A58, A56, A116, Th6, NAT_1:14 ;
hence g "**" H1 = g "**" H2 by A123; ::_thesis: verum
end;
suppose ( len q1 <> 0 & len q2 = 0 ) ; ::_thesis: g "**" H1 = g "**" H2
then A124: q2 = {} ;
then H1 = q1 ^ <*d*> by A97, FINSEQ_1:34
.= (q1 ^ q2) ^ <*d*> by A124, FINSEQ_1:34 ;
hence g "**" H1 = g "**" H2 by A17, A16, A58, A56, A116, A118, Th4, NAT_1:14; ::_thesis: verum
end;
suppose ( len q1 = 0 & len q2 = 0 ) ; ::_thesis: g "**" H1 = g "**" H2
then len (q1 ^ q2) = 0 + 0 by FINSEQ_1:22;
hence g "**" H1 = g "**" H2 by A5, A6, A17, A16, A56, A116, FINSEQ_1:17; ::_thesis: verum
end;
end;
end;
hence g "**" H1 = g "**" H2 ; ::_thesis: verum
end;
supposeA125: len p = 0 ; ::_thesis: g "**" H1 = g "**" H2
then dom H1 = {1} by A5, A58, FINSEQ_1:2, FINSEQ_1:def_3;
then A126: ( dom f = {1} & rng f = {1} ) by FUNCT_2:def_1, FUNCT_2:def_3;
1 in {1} by TARSKI:def_1;
then f . 1 in {1} by A126, FUNCT_1:def_3;
then H1 . 1 = H2 . 1 by A75, A58, A125, TARSKI:def_1;
then H1 = <*d*> by A5, A58, A125, FINSEQ_1:40;
hence g "**" H1 = g "**" H2 by A5, A6, A58, A125, FINSEQ_1:40; ::_thesis: verum
end;
end;
end;
hence g "**" H1 = g "**" H2 ; ::_thesis: verum
end;
end;
let f be Permutation of (dom F); ::_thesis: ( len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies g "**" F = g "**" G )
A127: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A127, A3);
hence ( len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies g "**" F = g "**" G ) ; ::_thesis: verum
end;
Lm8: for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D
for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
let g be BinOp of D; ::_thesis: for P being Permutation of (dom F) st g is having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
let P be Permutation of (dom F); ::_thesis: ( g is having_a_unity & len F = 0 & G = F * P implies g "**" F = g "**" G )
assume that
A1: g is having_a_unity and
A2: len F = 0 ; ::_thesis: ( not G = F * P or g "**" F = g "**" G )
assume A3: G = F * P ; ::_thesis: g "**" F = g "**" G
F = {} by A2;
then G = {} by A3, RELAT_1:39;
then A4: len G = 0 ;
thus g "**" F = the_unity_wrt g by A1, A2, Def1
.= g "**" G by A1, A4, Def1 ; ::_thesis: verum
end;
theorem Th7: :: FINSOP_1:7
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D
for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
let g be BinOp of D; ::_thesis: for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
let P be Permutation of (dom F); ::_thesis: ( g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P implies g "**" F = g "**" G )
assume that
A1: ( g is commutative & g is associative ) and
A2: ( g is having_a_unity or len F >= 1 ) ; ::_thesis: ( not G = F * P or g "**" F = g "**" G )
assume A3: G = F * P ; ::_thesis: g "**" F = g "**" G
now__::_thesis:_g_"**"_F_=_g_"**"_G
percases ( len F = 0 or len F <> 0 ) ;
suppose len F = 0 ; ::_thesis: g "**" F = g "**" G
hence g "**" F = g "**" G by A2, A3, Lm8; ::_thesis: verum
end;
supposeA4: len F <> 0 ; ::_thesis: g "**" F = g "**" G
( len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (P . i) ) ) by A3, FINSEQ_2:44, FUNCT_1:12;
hence g "**" F = g "**" G by A1, A4, Lm7, NAT_1:14; ::_thesis: verum
end;
end;
end;
hence g "**" F = g "**" G ; ::_thesis: verum
end;
Lm9: for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
let g be BinOp of D; ::_thesis: ( g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 implies g "**" F = g "**" G )
assume that
A1: ( g is associative & g is commutative ) and
A2: F is one-to-one and
A3: G is one-to-one and
A4: rng F = rng G and
A5: len F >= 1 ; ::_thesis: g "**" F = g "**" G
A6: len F = len G by A2, A3, A4, FINSEQ_1:48;
set P = (F ") * G;
A7: dom (F ") = rng F by A2, FUNCT_1:33;
then A8: dom ((F ") * G) = dom G by A4, RELAT_1:27
.= Seg (len F) by A6, FINSEQ_1:def_3
.= dom F by FINSEQ_1:def_3 ;
rng (F ") = dom F by A2, FUNCT_1:33;
then A9: rng ((F ") * G) c= dom F by RELAT_1:26;
dom F = Seg (len F) by FINSEQ_1:def_3;
then reconsider P = (F ") * G as Function of (dom F),(dom F) by A5, A8, A9, FUNCT_2:def_1, RELSET_1:4;
rng P = rng (F ") by A4, A7, RELAT_1:28
.= dom F by A2, FUNCT_1:33 ;
then reconsider P = P as Permutation of (dom F) by A2, A3, FUNCT_2:57;
F * P = (F * (F ")) * G by RELAT_1:36
.= (id (rng G)) * G by A2, A4, FUNCT_1:39
.= G by RELAT_1:54 ;
hence g "**" F = g "**" G by A1, A5, Th7; ::_thesis: verum
end;
Lm10: for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
let g be BinOp of D; ::_thesis: ( len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G )
assume that
A1: ( len F = 0 & g is having_a_unity ) and
A2: ( F is one-to-one & G is one-to-one & rng F = rng G ) ; ::_thesis: g "**" F = g "**" G
( len G = len F & g "**" F = the_unity_wrt g ) by A1, A2, Def1, FINSEQ_1:48;
hence g "**" F = g "**" G by A1, Def1; ::_thesis: verum
end;
theorem :: FINSOP_1:8
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
proof
let D be non empty set ; ::_thesis: for F, G being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
let F, G be FinSequence of D; ::_thesis: for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
let g be BinOp of D; ::_thesis: ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G )
( len F >= 1 or len F = 0 ) by NAT_1:14;
hence ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G ) by Lm9, Lm10; ::_thesis: verum
end;
Lm11: for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 1 holds
g "**" F = F . 1
proof
let D be non empty set ; ::_thesis: for F being FinSequence of D
for g being BinOp of D st len F = 1 holds
g "**" F = F . 1
let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 1 holds
g "**" F = F . 1
let g be BinOp of D; ::_thesis: ( len F = 1 implies g "**" F = F . 1 )
assume A1: len F = 1 ; ::_thesis: g "**" F = F . 1
then F = <*(F . 1)*> by FINSEQ_1:40
.= <*(F /. 1)*> by A1, FINSEQ_4:15 ;
hence g "**" F = F /. 1 by Lm4
.= F . 1 by A1, FINSEQ_4:15 ;
::_thesis: verum
end;
Lm12: for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ) holds
g "**" H = g . ((g "**" F),(g "**" G))
proof
let D be non empty set ; ::_thesis: for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ) holds
g "**" H = g . ((g "**" F),(g "**" G))
let F, G, H be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ) holds
g "**" H = g . ((g "**" F),(g "**" G))
let g be BinOp of D; ::_thesis: ( g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ) implies g "**" H = g . ((g "**" F),(g "**" G)) )
assume that
A1: g is associative and
A2: g is commutative ; ::_thesis: ( not len F >= 1 or not len F = len G or not len F = len H or ex k being Element of NAT st
( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) )
defpred S1[ Element of NAT ] means for F, G, H being FinSequence of D st len F >= 1 & len F = $1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ) holds
g "**" H = g . ((g "**" F),(g "**" G));
A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let F, G, H be FinSequence of D; ::_thesis: ( len F >= 1 & len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ) implies g "**" H = g . ((g "**" F),(g "**" G)) )
assume that
len F >= 1 and
A5: len F = k + 1 and
A6: len F = len G and
A7: len F = len H and
A8: for k being Element of NAT st k in dom F holds
H . k = g . ((F . k),(G . k)) ; ::_thesis: g "**" H = g . ((g "**" F),(g "**" G))
reconsider f = F | (Seg k), gg = G | (Seg k), h = H | (Seg k) as FinSequence of D by FINSEQ_1:18;
A9: len h = k by A5, A7, FINSEQ_3:53;
A10: len f = k by A5, FINSEQ_3:53;
A11: len gg = k by A5, A6, FINSEQ_3:53;
A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_
h_._i_=_g_._((f_._i),(gg_._i))
k <= k + 1 by NAT_1:12;
then Seg (len f) c= Seg (len F) by A5, A10, FINSEQ_1:5;
then Seg (len f) c= dom F by FINSEQ_1:def_3;
then A13: dom f c= dom F by FINSEQ_1:def_3;
let i be Element of NAT ; ::_thesis: ( i in dom f implies h . i = g . ((f . i),(gg . i)) )
assume A14: i in dom f ; ::_thesis: h . i = g . ((f . i),(gg . i))
then i in Seg (len gg) by A10, A11, FINSEQ_1:def_3;
then i in dom gg by FINSEQ_1:def_3;
then A15: G . i = gg . i by FUNCT_1:47;
i in Seg (len h) by A10, A9, A14, FINSEQ_1:def_3;
then i in dom h by FINSEQ_1:def_3;
then A16: H . i = h . i by FUNCT_1:47;
F . i = f . i by A14, FUNCT_1:47;
hence h . i = g . ((f . i),(gg . i)) by A8, A14, A15, A16, A13; ::_thesis: verum
end;
now__::_thesis:_g_"**"_H_=_g_._((g_"**"_F),(g_"**"_G))
percases ( len f >= 1 or len f = 0 ) by NAT_1:14;
supposeA17: len f >= 1 ; ::_thesis: g "**" H = g . ((g "**" F),(g "**" G))
A18: rng H c= D by FINSEQ_1:def_4;
A19: ( rng F c= D & rng G c= D ) by FINSEQ_1:def_4;
A20: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom G by A5, A6, FINSEQ_1:def_3;
then A21: G . (k + 1) in rng G by FUNCT_1:def_3;
k + 1 in dom H by A5, A7, A20, FINSEQ_1:def_3;
then A22: H . (k + 1) in rng H by FUNCT_1:def_3;
A23: k + 1 in dom F by A5, A20, FINSEQ_1:def_3;
then F . (k + 1) in rng F by FUNCT_1:def_3;
then reconsider d = F . (k + 1), d1 = G . (k + 1), d2 = H . (k + 1) as Element of D by A21, A22, A19, A18;
A24: d2 = g . ((F . (k + 1)),(G . (k + 1))) by A8, A23;
F = f ^ <*d*> by A5, FINSEQ_3:55;
then A25: g "**" F = g . ((g "**" f),d) by A17, Th4;
G = gg ^ <*d1*> by A5, A6, FINSEQ_3:55;
then A26: g "**" G = g . ((g "**" gg),d1) by A10, A11, A17, Th4;
A27: H = h ^ <*d2*> by A5, A7, FINSEQ_3:55;
g "**" h = g . ((g "**" f),(g "**" gg)) by A4, A10, A11, A9, A12, A17;
hence g "**" H = g . ((g . ((g "**" f),(g "**" gg))),(g . (d,d1))) by A10, A9, A17, A27, A24, Th4
.= g . ((g . ((g . ((g "**" f),(g "**" gg))),d)),d1) by A1, BINOP_1:def_3
.= g . ((g . ((g "**" f),(g . ((g "**" gg),d)))),d1) by A1, BINOP_1:def_3
.= g . ((g . ((g "**" f),(g . (d,(g "**" gg))))),d1) by A2, BINOP_1:def_2
.= g . ((g . ((g "**" F),(g "**" gg))),d1) by A1, A25, BINOP_1:def_3
.= g . ((g "**" F),(g "**" G)) by A1, A26, BINOP_1:def_3 ;
::_thesis: verum
end;
supposeA28: len f = 0 ; ::_thesis: g "**" H = g . ((g "**" F),(g "**" G))
then A29: ( g "**" G = G . 1 & 1 in dom F ) by A5, A6, A10, Lm11, FINSEQ_3:25;
( g "**" H = H . 1 & g "**" F = F . 1 ) by A5, A7, A10, A28, Lm11;
hence g "**" H = g . ((g "**" F),(g "**" G)) by A8, A29; ::_thesis: verum
end;
end;
end;
hence g "**" H = g . ((g "**" F),(g "**" G)) ; ::_thesis: verum
end;
end;
assume A30: ( len F >= 1 & len F = len G & len F = len H ) ; ::_thesis: ( ex k being Element of NAT st
( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) )
A31: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A31, A3);
hence ( ex k being Element of NAT st
( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) ) by A30; ::_thesis: verum
end;
Lm13: for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . ((g "**" G),(g "**" H))
proof
let D be non empty set ; ::_thesis: for F, G, H being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . ((g "**" G),(g "**" H))
let F, G, H be FinSequence of D; ::_thesis: for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . ((g "**" G),(g "**" H))
let g be BinOp of D; ::_thesis: ( g is having_a_unity & len F = 0 & len F = len G & len F = len H implies g "**" F = g . ((g "**" G),(g "**" H)) )
assume that
A1: g is having_a_unity and
A2: len F = 0 and
A3: len F = len G and
A4: len F = len H ; ::_thesis: g "**" F = g . ((g "**" G),(g "**" H))
thus g "**" F = the_unity_wrt g by A1, A2, Def1
.= g . ((the_unity_wrt g),(the_unity_wrt g)) by A1, SETWISEO:15
.= g . ((g "**" G),(the_unity_wrt g)) by A1, A2, A3, Def1
.= g . ((g "**" G),(g "**" H)) by A1, A2, A4, Def1 ; ::_thesis: verum
end;
theorem :: FINSOP_1:9
for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . ((G . k),(H . k)) ) holds
g "**" F = g . ((g "**" G),(g "**" H))
proof
let D be non empty set ; ::_thesis: for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . ((G . k),(H . k)) ) holds
g "**" F = g . ((g "**" G),(g "**" H))
let F, G, H be FinSequence of D; ::_thesis: for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . ((G . k),(H . k)) ) holds
g "**" F = g . ((g "**" G),(g "**" H))
let g be BinOp of D; ::_thesis: ( g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . ((G . k),(H . k)) ) implies g "**" F = g . ((g "**" G),(g "**" H)) )
A1: ( dom F = Seg (len F) & dom G = Seg (len G) ) by FINSEQ_1:def_3;
A2: ( len F = 0 or len F >= 1 ) by NAT_1:14;
assume ( g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) ) ; ::_thesis: ( not len F = len G or not len F = len H or ex k being Element of NAT st
( k in dom F & not F . k = g . ((G . k),(H . k)) ) or g "**" F = g . ((g "**" G),(g "**" H)) )
hence ( not len F = len G or not len F = len H or ex k being Element of NAT st
( k in dom F & not F . k = g . ((G . k),(H . k)) ) or g "**" F = g . ((g "**" G),(g "**" H)) ) by A1, A2, Lm12, Lm13; ::_thesis: verum
end;
theorem :: FINSOP_1:10
for D being non empty set
for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g by Lm3;
theorem :: FINSOP_1:11
for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d by Lm4;
theorem Th12: :: FINSOP_1:12
for D being non empty set
for d1, d2 being Element of D
for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2)
proof
let D be non empty set ; ::_thesis: for d1, d2 being Element of D
for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2)
let d1, d2 be Element of D; ::_thesis: for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2)
let g be BinOp of D; ::_thesis: g "**" <*d1,d2*> = g . (d1,d2)
A1: len <*d1*> = 1 by FINSEQ_1:39;
thus g "**" <*d1,d2*> = g "**" (<*d1*> ^ <*d2*>) by FINSEQ_1:def_9
.= g . ((g "**" <*d1*>),d2) by A1, Th4
.= g . (d1,d2) by Lm4 ; ::_thesis: verum
end;
theorem :: FINSOP_1:13
for D being non empty set
for d1, d2 being Element of D
for g being BinOp of D st g is commutative holds
g "**" <*d1,d2*> = g "**" <*d2,d1*>
proof
let D be non empty set ; ::_thesis: for d1, d2 being Element of D
for g being BinOp of D st g is commutative holds
g "**" <*d1,d2*> = g "**" <*d2,d1*>
let d1, d2 be Element of D; ::_thesis: for g being BinOp of D st g is commutative holds
g "**" <*d1,d2*> = g "**" <*d2,d1*>
let g be BinOp of D; ::_thesis: ( g is commutative implies g "**" <*d1,d2*> = g "**" <*d2,d1*> )
assume A1: g is commutative ; ::_thesis: g "**" <*d1,d2*> = g "**" <*d2,d1*>
thus g "**" <*d1,d2*> = g . (d1,d2) by Th12
.= g . (d2,d1) by A1, BINOP_1:def_2
.= g "**" <*d2,d1*> by Th12 ; ::_thesis: verum
end;
theorem Th14: :: FINSOP_1:14
for D being non empty set
for d1, d2, d3 being Element of D
for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
proof
let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D
for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
let d1, d2, d3 be Element of D; ::_thesis: for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
let g be BinOp of D; ::_thesis: g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
A1: len <*d1,d2*> = 2 by FINSEQ_1:44;
thus g "**" <*d1,d2,d3*> = g "**" (<*d1,d2*> ^ <*d3*>) by FINSEQ_1:43
.= g . ((g "**" <*d1,d2*>),d3) by A1, Th4
.= g . ((g . (d1,d2)),d3) by Th12 ; ::_thesis: verum
end;
theorem :: FINSOP_1:15
for D being non empty set
for d1, d2, d3 being Element of D
for g being BinOp of D st g is commutative holds
g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
proof
let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D
for g being BinOp of D st g is commutative holds
g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
let d1, d2, d3 be Element of D; ::_thesis: for g being BinOp of D st g is commutative holds
g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
let g be BinOp of D; ::_thesis: ( g is commutative implies g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*> )
assume A1: g is commutative ; ::_thesis: g "**" <*d1,d2,d3*> = g "**" <*d2,d1,d3*>
thus g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3) by Th14
.= g . ((g . (d2,d1)),d3) by A1, BINOP_1:def_2
.= g "**" <*d2,d1,d3*> by Th14 ; ::_thesis: verum
end;
theorem Th16: :: FINSOP_1:16
for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" (1 |-> d) = d
proof
let D be non empty set ; ::_thesis: for d being Element of D
for g being BinOp of D holds g "**" (1 |-> d) = d
let d be Element of D; ::_thesis: for g being BinOp of D holds g "**" (1 |-> d) = d
let g be BinOp of D; ::_thesis: g "**" (1 |-> d) = d
thus g "**" (1 |-> d) = g "**" <*d*> by FINSEQ_2:59
.= d by Lm4 ; ::_thesis: verum
end;
theorem :: FINSOP_1:17
for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" (2 |-> d) = g . (d,d)
proof
let D be non empty set ; ::_thesis: for d being Element of D
for g being BinOp of D holds g "**" (2 |-> d) = g . (d,d)
let d be Element of D; ::_thesis: for g being BinOp of D holds g "**" (2 |-> d) = g . (d,d)
let g be BinOp of D; ::_thesis: g "**" (2 |-> d) = g . (d,d)
thus g "**" (2 |-> d) = g "**" <*d,d*> by FINSEQ_2:61
.= g . (d,d) by Th12 ; ::_thesis: verum
end;
theorem Th18: :: FINSOP_1:18
for D being non empty set
for d being Element of D
for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d)))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d)))
let d be Element of D; ::_thesis: for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d)))
let g be BinOp of D; ::_thesis: for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d)))
let k, l be Element of NAT ; ::_thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) )
( k <> 0 & l <> 0 implies ( len (k |-> d) <> 0 & len (l |-> d) <> 0 ) ) by CARD_1:def_7;
then A1: ( k <> 0 & l <> 0 implies ( len (k |-> d) >= 1 & len (l |-> d) >= 1 ) ) by NAT_1:14;
(k + l) |-> d = (k |-> d) ^ (l |-> d) by FINSEQ_2:123;
hence ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k + l) |-> d) = g . ((g "**" (k |-> d)),(g "**" (l |-> d))) ) by A1, Th5; ::_thesis: verum
end;
theorem :: FINSOP_1:19
for D being non empty set
for d being Element of D
for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
proof
let D be non empty set ; ::_thesis: for d being Element of D
for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
let d be Element of D; ::_thesis: for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
let g be BinOp of D; ::_thesis: for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
let k, l be Element of NAT ; ::_thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) )
defpred S1[ Element of NAT ] means for g being BinOp of D
for k being Element of NAT
for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & $1 <> 0 ) ) holds
g "**" ((k * $1) |-> d) = g "**" ($1 |-> (g "**" (k |-> d)));
A1: for l being Element of NAT st S1[l] holds
S1[l + 1]
proof
let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A2: S1[l] ; ::_thesis: S1[l + 1]
let g be BinOp of D; ::_thesis: for k being Element of NAT
for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) holds
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
let k be Element of NAT ; ::_thesis: for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) holds
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
let d be Element of D; ::_thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) implies g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) )
assume that
A3: g is associative and
A4: ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) ; ::_thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
now__::_thesis:_g_"**"_((k_*_(l_+_1))_|->_d)_=_g_"**"_((l_+_1)_|->_(g_"**"_(k_|->_d)))
percases ( l = 0 or l <> 0 ) ;
suppose l = 0 ; ::_thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) by Th16; ::_thesis: verum
end;
supposeA5: l <> 0 ; ::_thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
then A6: ( k <> 0 implies k * l <> 0 ) by XCMPLX_1:6;
g "**" ((k * (l + 1)) |-> d) = g "**" (((k * l) + (k * 1)) |-> d)
.= g . ((g "**" ((k * l) |-> d)),(g "**" (k |-> d))) by A3, A4, A6, Th18
.= g . ((g "**" (l |-> (g "**" (k |-> d)))),(g "**" (k |-> d))) by A2, A3, A4, A5
.= g . ((g "**" (l |-> (g "**" (k |-> d)))),(g "**" (1 |-> (g "**" (k |-> d))))) by Th16 ;
hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) by A3, A5, Th18; ::_thesis: verum
end;
end;
end;
hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) ; ::_thesis: verum
end;
A7: S1[ 0 ] ;
for l being Element of NAT holds S1[l] from NAT_1:sch_1(A7, A1);
hence ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) ) ; ::_thesis: verum
end;
theorem :: FINSOP_1:20
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 1 holds
g "**" F = F . 1 by Lm11;
theorem :: FINSOP_1:21
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 2 holds
g "**" F = g . ((F . 1),(F . 2))
proof
let D be non empty set ; ::_thesis: for F being FinSequence of D
for g being BinOp of D st len F = 2 holds
g "**" F = g . ((F . 1),(F . 2))
let F be FinSequence of D; ::_thesis: for g being BinOp of D st len F = 2 holds
g "**" F = g . ((F . 1),(F . 2))
let g be BinOp of D; ::_thesis: ( len F = 2 implies g "**" F = g . ((F . 1),(F . 2)) )
assume A1: len F = 2 ; ::_thesis: g "**" F = g . ((F . 1),(F . 2))
then F = <*(F . 1),(F . 2)*> by FINSEQ_1:44
.= <*(F /. 1),(F . 2)*> by A1, FINSEQ_4:15
.= <*(F /. 1),(F /. 2)*> by A1, FINSEQ_4:15 ;
hence g "**" F = g . ((F /. 1),(F /. 2)) by Th12
.= g . ((F . 1),(F /. 2)) by A1, FINSEQ_4:15
.= g . ((F . 1),(F . 2)) by A1, FINSEQ_4:15 ;
::_thesis: verum
end;