:: AUTALG_1 semantic presentation

theorem Th1: :: AUTALG_1:1

for b₁ being Universal_Algebra holds id the carrier of b₁ is_isomorphism b₁,b₁

let c₁ be Universal_Algebra;
set c₂ = id the carrier of c₁;
thus id the carrier of c₁ is_monomorphism c₁,c₁ :: according to ALG_1:def 4

proof

thus id the carrier of c₁ is_homomorphism c₁,c₁ by ALG_1:6; :: according to ALG_1:def 2
thus id the carrier of c₁ is one-to-one ;

end;

thus id the carrier of c₁ is_epimorphism c₁,c₁

proof

thus id the carrier of c₁ is_homomorphism c₁,c₁ by ALG_1:6; :: according to ALG_1:def 3
thus rng (id the carrier of c₁) = the carrier of c₁ by RELAT_1:71;

end;

definition

let c₁ be Universal_Algebra;
func UAAut c₁ -> FUNCTION_DOMAIN of the carrier of a₁,the carrier of a₁ means :Def1: :: AUTALG_1:def 1
( ( for b₁ being Element of a₂ holds
b₁ is Function of a₁,a₁ ) & ( for b₁ being Function of a₁,a₁ holds
( b₁ in a₂ iff b₁ is_isomorphism a₁,a₁ ) ) );
existence

proof

set c₂ = { b₁ where B is Element of Funcs the carrier of c₁,the carrier of c₁ : b₁ is_isomorphism c₁,c₁ } ;
E2: id the carrier of c₁ in { b₁ where B is Element of Funcs the carrier of c₁,the carrier of c₁ : b₁ is_isomorphism c₁,c₁ }

proof

set c₃ = id the carrier of c₁;
E3: id the carrier of c₁ in Funcs the carrier of c₁,the carrier of c₁ by FUNCT_2:11;
id the carrier of c₁ is_isomorphism c₁,c₁ by Th1;
hence id the carrier of c₁ in { b₁ where B is Element of Funcs the carrier of c₁,the carrier of c₁ : b₁ is_isomorphism c₁,c₁ } by E3;

end;

reconsider c₃ = { b₁ where B is Element of Funcs the carrier of c₁,the carrier of c₁ : b₁ is_isomorphism c₁,c₁ } as set ;
c₃ is functional

proof

let c₄ be set ; :: according to FRAENKEL:def 1
assume c₄ in c₃ ;
then consider c₅ being Element of Funcs the carrier of c₁,the carrier of c₁ such that
E3: ( c₄ = c₅ & c₅ is_isomorphism c₁,c₁ ) ;
thus c₄ is set by E3;

end;

then reconsider c₄ = c₃ as non empty functional set by E2;
c₄ is FUNCTION_DOMAIN of the carrier of c₁,the carrier of c₁

proof

let c₅ be Element of c₄; :: according to FRAENKEL:def 2
c₅ in c₄ ;
then consider c₆ being Element of Funcs the carrier of c₁,the carrier of c₁ such that
E3: ( c₅ = c₆ & c₆ is_isomorphism c₁,c₁ ) ;
thus c₅ is M5(the carrier of c₁,the carrier of c₁) by E3;

end;

then reconsider c₅ = c₄ as FUNCTION_DOMAIN of the carrier of c₁,the carrier of c₁ ;
take c₅ ;
thus for b₁ being Element of c₅ holds
b₁ is Function of c₁,c₁ ;
let c₆ be Function of c₁,c₁;
thus ( c₆ in c₅ implies c₆ is_isomorphism c₁,c₁ )

proof

assume c₆ in c₅ ;
then ex b₁ being Element of Funcs the carrier of c₁,the carrier of c₁ st
( b₁ = c₆ & b₁ is_isomorphism c₁,c₁ ) ;
hence c₆ is_isomorphism c₁,c₁ ;

end;

assume E3: c₆ is_isomorphism c₁,c₁ ;
c₆ is Element of Funcs the carrier of c₁,the carrier of c₁ by FUNCT_2:11;
hence c₆ in c₅ by E3;

end;

uniqueness

proof

let c₂, c₃ be FUNCTION_DOMAIN of the carrier of c₁,the carrier of c₁;
assume that
E2: ( ( for b₁ being Element of c₂ holds
b₁ is Function of c₁,c₁ ) & ( for b₁ being Function of c₁,c₁ holds
( b₁ in c₂ iff b₁ is_isomorphism c₁,c₁ ) ) ) and
E3: ( ( for b₁ being Element of c₃ holds
b₁ is Function of c₁,c₁ ) & ( for b₁ being Function of c₁,c₁ holds
( b₁ in c₃ iff b₁ is_isomorphism c₁,c₁ ) ) ) ;
E4: c₂ c= c₃

proof

let c₄ be set ; :: according to TARSKI:def 3
assume E5: c₄ in c₂ ;
then reconsider c₅ = c₄ as Function of c₁,c₁ by E2;
c₅ is_isomorphism c₁,c₁ by E2, E5;
hence c₄ in c₃ by E3;

end;

c₃ c= c₂

proof

let c₄ be set ; :: according to TARSKI:def 3
assume E5: c₄ in c₃ ;
then reconsider c₅ = c₄ as Function of c₁,c₁ by E3;
c₅ is_isomorphism c₁,c₁ by E3, E5;
hence c₄ in c₂ by E2;

end;

hence c₂ = c₃ by E4, XBOOLE_0:def 10;

end;

:: deftheorem Def1 defines UAAut AUTALG_1:def 1 :

theorem Th2: :: AUTALG_1:2

for b₁ being Universal_Algebra holds UAAut b₁ c= Funcs the carrier of b₁,the carrier of b₁

proof

let c₁ be Universal_Algebra;
let c₂ be set ; :: according to TARSKI:def 3
assume c₂ in UAAut c₁ ;
then consider c₃ being Element of UAAut c₁ such that
E3: c₃ = c₂ ;
thus c₂ in Funcs the carrier of c₁,the carrier of c₁ by E3, FUNCT_2:12;

end;

theorem Th3: :: AUTALG_1:3

canceled;

theorem Th4: :: AUTALG_1:4

for b₁ being Universal_Algebra holds id the carrier of b₁ in UAAut b₁

proof

let c₁ be Universal_Algebra;
id the carrier of c₁ is_isomorphism c₁,c₁ by Th1;
hence id the carrier of c₁ in UAAut c₁ by Def1;

end;

theorem Th5: :: AUTALG_1:5

for b₁ being Universal_Algebra
for b₂, b₃ being Function of b₁,b₁ holds
( b₂ is Element of UAAut b₁ & b₃ = b₂ " implies b₃ is_isomorphism b₁,b₁ )

proof

let c₁ be Universal_Algebra;
let c₂, c₃ be Function of c₁,c₁;
assume E4: ( c₂ is Element of UAAut c₁ & c₃ = c₂ " ) ;
then c₂ is_isomorphism c₁,c₁ by Def1;
hence c₃ is_isomorphism c₁,c₁ by E4, ALG_1:11;

end;

Lemma4: for b₁ being Universal_Algebra
for b₂ being Function of b₁,b₁ holds
( b₂ is_isomorphism b₁,b₁ implies b₂ " is Function of b₁,b₁ )

proof

let c₁ be Universal_Algebra;
let c₂ be Function of c₁,c₁;
assume E5: c₂ is_isomorphism c₁,c₁ ;
then E6: c₂ is one-to-one by ALG_1:8;
c₂ is_epimorphism c₁,c₁ by E5, ALG_1:def 4;
then rng c₂ = the carrier of c₁ by ALG_1:def 3;
hence c₂ " is Function of c₁,c₁ by E6, FUNCT_2:31;

end;

theorem Th6: :: AUTALG_1:6

for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁ holds b₂ " in UAAut b₁

proof

let c₁ be Universal_Algebra;
let c₂ be Element of UAAut c₁;
E6: c₂ is_isomorphism c₁,c₁ by Def1;
then c₂ " is Function of c₁,c₁ by Lemma4;
then consider c₃ being Function of c₁,c₁ such that
E7: c₃ = c₂ " ;
c₃ is_isomorphism c₁,c₁ by E6, E7, ALG_1:11;
hence c₂ " in UAAut c₁ by E7, Def1;

end;

theorem Th7: :: AUTALG_1:7

for b₁ being Universal_Algebra
for b₂, b₃ being Element of UAAut b₁ holds b₂ * b₃ in UAAut b₁

proof

let c₁ be Universal_Algebra;
let c₂, c₃ be Element of UAAut c₁;
( c₂ is_isomorphism c₁,c₁ & c₃ is_isomorphism c₁,c₁ ) by Def1;
then c₂ * c₃ is_isomorphism c₁,c₁ by ALG_1:12;
hence c₂ * c₃ in UAAut c₁ by Def1;

end;

definition

let c₁ be Universal_Algebra;
func UAAutComp c₁ -> BinOp of UAAut a₁ means :Def2: :: AUTALG_1:def 2
for b₁, b₂ being Element of UAAut a₁ holds a₂ . b₁,b₂ = b₂ * b₁;
existence

proof

defpred S₁[ Element of UAAut c₁, Element of UAAut c₁, set ] means a₃ = a₂ * a₁;
E7: for b₁, b₂ being Element of UAAut c₁ holds
ex b₃ being Element of UAAut c₁ st
S₁[b₁,b₂,b₃]

proof

let c₂, c₃ be Element of UAAut c₁;
reconsider c₄ = c₂, c₅ = c₃ as Function of c₁,c₁ ;
reconsider c₆ = c₅ * c₄ as Element of UAAut c₁ by Th7;
take c₆ ;
thus S₁[c₂,c₃,c₆] ;

end;

thus ex b₁ being BinOp of UAAut c₁ st
for b₂, b₃ being Element of UAAut c₁ holds
S₁[b₂,b₃,b₁ . b₂,b₃] from BINOP_1:sch 3(E7);

end;

uniqueness

proof

let c₂, c₃ be BinOp of UAAut c₁;
assume that
E7: for b₁, b₂ being Element of UAAut c₁ holds c₂ . b₁,b₂ = b₂ * b₁ and
E8: for b₁, b₂ being Element of UAAut c₁ holds c₃ . b₁,b₂ = b₂ * b₁ ;
for b₁, b₂ being Element of UAAut c₁ holds c₂ . b₁,b₂ = c₃ . b₁,b₂

proof

let c₄, c₅ be Element of UAAut c₁;
thus c₂ . c₄,c₅ = c₅ * c₄ by E7
.= c₃ . c₄,c₅ by E8 ;

end;

hence c₂ = c₃ by BINOP_1:2;

end;

:: deftheorem Def2 defines UAAutComp AUTALG_1:def 2 :

definition

let c₁ be Universal_Algebra;
func UAAutGroup c₁ -> Group equals :: AUTALG_1:def 3
HGrStr(# (UAAut a₁),(UAAutComp a₁) #);
coherence

proof

set c₂ = HGrStr(# (UAAut c₁),(UAAutComp c₁) #);
( HGrStr(# (UAAut c₁),(UAAutComp c₁) #) is associative & HGrStr(# (UAAut c₁),(UAAutComp c₁) #) is Group-like )

proof

E8: for b₁, b₂ being Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #)
for b₃, b₄ being Element of UAAut c₁ holds
( b₁ = b₃ & b₂ = b₄ implies b₁ * b₂ = b₄ * b₃ ) by Def2;
thus for b₁, b₂, b₃ being Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) :: according to GROUP_1:def 4

proof

let c₃, c₄, c₅ be Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #);
reconsider c₆ = c₃, c₇ = c₄, c₈ = c₅ as Element of UAAut c₁ ;
E9: c₃ * c₄ = c₇ * c₆ by E8;
E10: c₄ * c₅ = c₈ * c₇ by E8;
thus (c₃ * c₄) * c₅ = c₈ * (c₇ * c₆) by E8, E9
.= (c₈ * c₇) * c₆ by RELAT_1:55
.= c₃ * (c₄ * c₅) by E8, E10 ;

end;

thus ex b₁ being Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #) st
for b₂ being Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #) holds
( b₂ * b₁ = b₂ & b₁ * b₂ = b₂ & ex b₃ being Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #) st
( b₂ * b₃ = b₁ & b₃ * b₂ = b₁ ) ) :: according to GROUP_1:def 3

proof

reconsider c₃ = id the carrier of c₁ as Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #) by Th4;
take c₃ ;
let c₄ be Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #);
consider c₅ being Element of UAAut c₁ such that
E9: c₅ = c₄ ;
c₄ * c₃ = (id the carrier of c₁) * c₅ by E8, E9
.= c₅ by FUNCT_2:23 ;
hence c₄ * c₃ = c₄ by E9;
c₃ * c₄ = c₅ * (id the carrier of c₁) by E8, E9
.= c₅ by FUNCT_2:23 ;
hence c₃ * c₄ = c₄ by E9;
reconsider c₆ = c₅ " as Element of HGrStr(# (UAAut c₁),(UAAutComp c₁) #) by Th6;
take c₆ ;
E10: c₅ is_isomorphism c₁,c₁ by Def1;
then E11: c₅ is one-to-one by ALG_1:8;
c₅ is_epimorphism c₁,c₁ by E10, ALG_1:def 4;
then E12: rng c₅ = the carrier of c₁ by ALG_1:def 3;
thus c₄ * c₆ = (c₅ " ) * c₅ by E8, E9
.= c₃ by E11, E12, FUNCT_2:35 ;
thus c₆ * c₄ = c₅ * (c₅ " ) by E8, E9
.= c₃ by E11, E12, FUNCT_2:35 ;

end;

hence HGrStr(# (UAAut c₁),(UAAutComp c₁) #) is Group ;

end;

:: deftheorem Def3 defines UAAutGroup AUTALG_1:def 3 :

registration

let c₁ be Universal_Algebra;
cluster UAAutGroup a₁ -> strict ;
coherence ;

end;

Lemma8: for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁ holds
( dom b₂ = rng b₂ & dom b₂ = the carrier of b₁ )

proof

let c₁ be Universal_Algebra;
let c₂ be Element of UAAut c₁;
c₂ is_isomorphism c₁,c₁ by Def1;
then ( dom c₂ = the carrier of c₁ & rng c₂ = the carrier of c₁ ) by ALG_1:9;
hence ( dom c₂ = rng c₂ & dom c₂ = the carrier of c₁ ) ;

end;

theorem Th8: :: AUTALG_1:8

for b₁ being Universal_Algebra
for b₂, b₃ being Element of (UAAutGroup b₁)
for b₄, b₅ being Element of UAAut b₁ holds
( b₂ = b₄ & b₃ = b₅ implies b₂ * b₃ = b₅ * b₄ ) by Def2;

theorem Th9: :: AUTALG_1:9

for b₁ being Universal_Algebra holds id the carrier of b₁ = 1. (UAAutGroup b₁)

proof

let c₁ be Universal_Algebra;
reconsider c₂ = id the carrier of c₁ as Element of (UAAutGroup c₁) by Th4;
consider c₃ being Function of the carrier of c₁,the carrier of c₁ such that
E11: c₃ = c₂ ;
consider c₄ being Element of (UAAutGroup c₁);
c₄ is Element of UAAut c₁ ;
then consider c₅ being Function of the carrier of c₁,the carrier of c₁ such that
E12: c₅ = c₄ ;
c₂ * c₄ = c₅ * c₃ by E11, E12, Th8
.= c₄ by E11, E12, FUNCT_2:23 ;
hence id the carrier of c₁ = 1. (UAAutGroup c₁) by GROUP_1:15;

end;

theorem Th10: :: AUTALG_1:10

for b₁ being Universal_Algebra
for b₂ being Element of UAAut b₁
for b₃ being Element of (UAAutGroup b₁) holds
( b₂ = b₃ implies b₂ " = b₃ " )

proof

let c₁ be Universal_Algebra;
let c₂ be Element of UAAut c₁;
let c₃ be Element of (UAAutGroup c₁);
assume E11: c₂ = c₃ ;
consider c₄ being Element of UAAut c₁ such that
E12: c₄ = c₃ " ;
E13: rng c₂ = dom c₂ by Lemma8
.= the carrier of c₁ by Lemma8 ;
c₂ is_isomorphism c₁,c₁ by Def1;
then c₂ is_monomorphism c₁,c₁ by ALG_1:def 4;
then E14: c₂ is one-to-one by ALG_1:def 2;
c₄ * c₂ = c₃ * (c₃ " ) by E11, E12, Th8;
then c₄ * c₂ = 1. (UAAutGroup c₁) by GROUP_1:def 6;
then c₄ * c₂ = id the carrier of c₁ by Th9;
hence c₂ " = c₃ " by E12, E13, E14, FUNCT_2:36;

end;

theorem Th11: :: AUTALG_1:11

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( b₂ is_transformable_to b₃ & b₃ is_transformable_to b₄ implies b₂ is_transformable_to b₄ )

proof

let c₁ be set ;
let c₂, c₃, c₄ be ManySortedSet of c₁;
assume E11: ( c₂ is_transformable_to c₃ & c₃ is_transformable_to c₄ ) ;
thus c₂ is_transformable_to c₄

proof

let c₅ be set ; :: according to PZFMISC1:def 3
assume c₅ in c₁ ;
then ( ( c₃ . c₅ = {} implies c₂ . c₅ = {} ) & ( c₄ . c₅ = {} implies c₃ . c₅ = {} ) ) by E11, PZFMISC1:def 3;
hence ( c₄ . c₅ = {} implies c₂ . c₅ = {} ) ;

end;

theorem Th12: :: AUTALG_1:12

for b₁ being set
for b₂ being ManySortedSet of {b₁} holds b₂ = b₁ .--> (b₂ . b₁)

proof

let c₁ be set ;
let c₂ be ManySortedSet of {c₁};
E12: dom c₂ = {c₁} by PBOOLE:def 3;
then rng c₂ = {(c₂ . c₁)} by FUNCT_1:14;
hence c₂ = c₁ .--> (c₂ . c₁) by E12, FUNCOP_1:15;

end;

theorem Th13: :: AUTALG_1:13

for b₁, b₂, b₃ being Function-yielding Function holds (b₃ ** b₂) ** b₁ = b₃ ** (b₂ ** b₁)

proof

let c₁, c₂, c₃ be Function-yielding Function;
set c₄ = (c₃ ** c₂) ** c₁;
set c₅ = c₃ ** (c₂ ** c₁);

now

E13: dom ((c₃ ** c₂) ** c₁) = (dom (c₃ ** c₂)) /\ (dom c₁) by PBOOLE:def 24
.= ((dom c₃) /\ (dom c₂)) /\ (dom c₁) by PBOOLE:def 24 ;
then E14: dom ((c₃ ** c₂) ** c₁) = (dom c₃) /\ ((dom c₂) /\ (dom c₁)) by XBOOLE_1:16;
hence E15: dom ((c₃ ** c₂) ** c₁) = (dom c₃) /\ (dom (c₂ ** c₁)) by PBOOLE:def 24
.= dom (c₃ ** (c₂ ** c₁)) by PBOOLE:def 24 ;

let c₆ be set ;
assume E16: c₆ in dom ((c₃ ** c₂) ** c₁) ;
then c₆ in (dom c₃) /\ (dom c₂) by E13, XBOOLE_0:def 3;
then E17: c₆ in dom (c₃ ** c₂) by PBOOLE:def 24;
c₆ in (dom c₂) /\ (dom c₁) by E14, E16, XBOOLE_0:def 3;
then E18: c₆ in dom (c₂ ** c₁) by PBOOLE:def 24;
thus ((c₃ ** c₂) ** c₁) . c₆ = ((c₃ ** c₂) . c₆) * (c₁ . c₆) by E16, PBOOLE:def 24
.= ((c₃ . c₆) * (c₂ . c₆)) * (c₁ . c₆) by E17, PBOOLE:def 24
.= (c₃ . c₆) * ((c₂ . c₆) * (c₁ . c₆)) by RELAT_1:55
.= (c₃ . c₆) * ((c₂ ** c₁) . c₆) by E18, PBOOLE:def 24
.= (c₃ ** (c₂ ** c₁)) . c₆ by E15, E16, PBOOLE:def 24 ;

end;

hence (c₃ ** c₂) ** c₁ = c₃ ** (c₂ ** c₁) by FUNCT_1:9;

end;

theorem Th14: :: AUTALG_1:14

for b₁ being set
for b₂, b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃ holds
( b₄ is "1-1" & b₄ is "onto" implies ( b₄ "" is "1-1" & b₄ "" is "onto" ) )

proof

let c₁ be set ;
let c₂, c₃ be V2 ManySortedSet of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
assume E14: ( c₄ is "1-1" & c₄ is "onto" ) ;

now

let c₅ be set ;
assume E15: c₅ in c₁ ;
then reconsider c₆ = c₄ . c₅ as Function of c₂ . c₅,c₃ . c₅ by PBOOLE:def 18;
c₆ is one-to-one by E14, E15, MSUALG_3:1;
then c₆ " is one-to-one by FUNCT_1:62;
hence (c₄ "" ) . c₅ is one-to-one by E14, E15, MSUALG_3:def 5;

end;

hence c₄ "" is "1-1" by MSUALG_3:1;
thus c₄ "" is "onto"

proof

let c₅ be set ; :: according to MSUALG_3:def 3
assume E15: c₅ in c₁ ;
then E16: ( c₂ . c₅ <> {} & c₃ . c₅ <> {} ) by PBOOLE:def 16;
reconsider c₆ = c₄ . c₅ as Function of c₂ . c₅,c₃ . c₅ by E15, PBOOLE:def 18;
E17: c₆ is one-to-one by E14, E15, MSUALG_3:1;
c₂ . c₅ = dom c₆ by E16, FUNCT_2:def 1
.= rng (c₆ " ) by E17, FUNCT_1:55 ;
hence rng ((c₄ "" ) . c₅) = c₂ . c₅ by E14, E15, MSUALG_3:def 5;

end;

theorem Th15: :: AUTALG_1:15

for b₁ being set
for b₂, b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃ holds
( b₄ is "1-1" & b₄ is "onto" implies (b₄ "" ) "" = b₄ )

proof

let c₁ be set ;
let c₂, c₃ be V2 ManySortedSet of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
assume E14: ( c₄ is "1-1" & c₄ is "onto" ) ;

now

let c₅ be set ;
assume E15: c₅ in c₁ ;
then reconsider c₆ = (c₄ "" ) . c₅ as Function of c₃ . c₅,c₂ . c₅ by PBOOLE:def 18;
reconsider c₇ = c₄ . c₅ as Function of c₂ . c₅,c₃ . c₅ by E15, PBOOLE:def 18;
( c₄ "" is "1-1" & c₄ "" is "onto" ) by E14, Th14;
then E16: ((c₄ "" ) "" ) . c₅ = c₆ " by E15, MSUALG_3:def 5;
c₇ is one-to-one by E14, E15, MSUALG_3:1;
then (c₇ " ) " = c₇ by FUNCT_1:65;
hence ((c₄ "" ) "" ) . c₅ = c₄ . c₅ by E14, E15, E16, MSUALG_3:def 5;

end;

hence (c₄ "" ) "" = c₄ by PBOOLE:3;

end;

theorem Th16: :: AUTALG_1:16

for b₁, b₂ being Function-yielding Function holds
( b₁ is "1-1" & b₂ is "1-1" implies b₂ ** b₁ is "1-1" )

proof

let c₁, c₂ be Function-yielding Function;
assume E15: ( c₁ is "1-1" & c₂ is "1-1" ) ;
let c₃ be set ; :: according to MSUALG_3:def 2
let c₄ be Function;
assume that
E16: c₃ in dom (c₂ ** c₁) and
E17: (c₂ ** c₁) . c₃ = c₄ ;
dom (c₂ ** c₁) = (dom c₂) /\ (dom c₁) by PBOOLE:def 24;
then ( c₃ in dom c₂ & c₃ in dom c₁ ) by E16, XBOOLE_0:def 3;
then ( c₂ . c₃ is one-to-one & c₁ . c₃ is one-to-one ) by E15, MSUALG_3:def 2;
then (c₂ . c₃) * (c₁ . c₃) is one-to-one by FUNCT_1:46;
hence c₄ is one-to-one by E16, E17, PBOOLE:def 24;

end;

theorem Th17: :: AUTALG_1:17

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ holds
( b₅ is "onto" & b₆ is "onto" implies b₆ ** b₅ is "onto" )

proof

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be V2 ManySortedSet of c₁;
let c₅ be ManySortedFunction of c₂,c₃;
let c₆ be ManySortedFunction of c₃,c₄;
assume that
E16: c₅ is "onto" and
E17: c₆ is "onto" ;

now

let c₇ be set ;
assume E18: c₇ in c₁ ;
then reconsider c₈ = c₅ . c₇ as Function of c₂ . c₇,c₃ . c₇ by PBOOLE:def 18;
reconsider c₉ = c₆ . c₇ as Function of c₃ . c₇,c₄ . c₇ by E18, PBOOLE:def 18;
E19: c₃ . c₇ <> {} by E18, PBOOLE:def 16;
E20: c₄ . c₇ <> {} by E18, PBOOLE:def 16;
( rng c₈ = c₃ . c₇ & rng c₉ = c₄ . c₇ ) by E16, E17, E18, MSUALG_3:def 3;
then rng (c₉ * c₈) = c₄ . c₇ by E19, E20, FUNCT_2:20;
hence rng ((c₆ ** c₅) . c₇) = c₄ . c₇ by E18, MSUALG_3:2;

end;

hence c₆ ** c₅ is "onto" by MSUALG_3:def 3;

end;

theorem Th18: :: AUTALG_1:18

for b₁ being set
for b₂, b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ holds
( b₅ is "1-1" & b₅ is "onto" & b₆ is "1-1" & b₆ is "onto" implies (b₆ ** b₅) "" = (b₅ "" ) ** (b₆ "" ) )

proof

let c₁ be set ;
let c₂, c₃, c₄ be V2 ManySortedSet of c₁;
let c₅ be ManySortedFunction of c₂,c₃;
let c₆ be ManySortedFunction of c₃,c₄;
assume that
E16: ( c₅ is "1-1" & c₅ is "onto" ) and
E17: ( c₆ is "1-1" & c₆ is "onto" ) ;

now

let c₇ be set ;
assume E18: c₇ in c₁ ;
then reconsider c₈ = c₅ . c₇ as Function of c₂ . c₇,c₃ . c₇ by PBOOLE:def 18;
reconsider c₉ = c₆ . c₇ as Function of c₃ . c₇,c₄ . c₇ by E18, PBOOLE:def 18;
E19: (c₅ "" ) . c₇ = c₈ " by E16, E18, MSUALG_3:def 5;
E20: (c₆ "" ) . c₇ = c₉ " by E17, E18, MSUALG_3:def 5;
E21: ( c₆ ** c₅ is "1-1" & c₆ ** c₅ is "onto" ) by E16, E17, Th16, Th17;
E22: c₈ is one-to-one by E16, E18, MSUALG_3:1;
E23: c₉ is one-to-one by E17, E18, MSUALG_3:1;
(c₆ ** c₅) . c₇ = c₉ * c₈ by E18, MSUALG_3:2;
then E24: ((c₆ ** c₅) "" ) . c₇ = (c₉ * c₈) " by E18, E21, MSUALG_3:def 5;
rng c₈ = c₃ . c₇ by E16, E18, MSUALG_3:def 3;
then reconsider c₁₀ = (c₅ "" ) . c₇ as Function of c₃ . c₇,c₂ . c₇ by E19, E22, FUNCT_2:31;
rng c₉ = c₄ . c₇ by E17, E18, MSUALG_3:def 3;
then reconsider c₁₁ = (c₆ "" ) . c₇ as Function of c₄ . c₇,c₃ . c₇ by E20, E23, FUNCT_2:31;
((c₅ "" ) ** (c₆ "" )) . c₇ = c₁₀ * c₁₁ by E18, MSUALG_3:2
.= c₁₀ * (c₉ " ) by E17, E18, MSUALG_3:def 5
.= (c₈ " ) * (c₉ " ) by E16, E18, MSUALG_3:def 5 ;
hence ((c₆ ** c₅) "" ) . c₇ = ((c₅ "" ) ** (c₆ "" )) . c₇ by E22, E23, E24, FUNCT_1:66;

end;

hence (c₆ ** c₅) "" = (c₅ "" ) ** (c₆ "" ) by PBOOLE:3;

end;

theorem Th19: :: AUTALG_1:19

for b₁ being set
for b₂, b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃
for b₅ being ManySortedFunction of b₃,b₂ holds
( b₄ is "1-1" & b₄ is "onto" & b₅ ** b₄ = id b₂ implies b₅ = b₄ "" )

proof

let c₁ be set ;
let c₂, c₃ be V2 ManySortedSet of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
let c₅ be ManySortedFunction of c₃,c₂;
assume E17: ( c₄ is "1-1" & c₄ is "onto" & c₅ ** c₄ = id c₂ ) ;

now

let c₆ be set ;
assume E18: c₆ in c₁ ;
then reconsider c₇ = c₄ . c₆ as Function of c₂ . c₆,c₃ . c₆ by PBOOLE:def 18;
reconsider c₈ = c₅ . c₆ as Function of c₃ . c₆,c₂ . c₆ by E18, PBOOLE:def 18;
E19: (c₄ "" ) . c₆ = c₇ " by E17, E18, MSUALG_3:def 5;

now

thus c₂ . c₆ <> {} by E18, PBOOLE:def 16;
thus c₃ . c₆ <> {} by E18, PBOOLE:def 16;
thus rng c₇ = c₃ . c₆ by E17, E18, MSUALG_3:def 3;
(c₅ ** c₄) . c₆ = id (c₂ . c₆) by E17, E18, MSUALG_3:def 1;
hence c₈ * c₇ = id (c₂ . c₆) by E18, MSUALG_3:2;
thus c₇ is one-to-one by E17, E18, MSUALG_3:1;

end;

hence c₅ . c₆ = (c₄ "" ) . c₆ by E19, FUNCT_2:36;

end;

hence c₅ = c₄ "" by PBOOLE:3;

end;

theorem Th20: :: AUTALG_1:20

canceled;

theorem Th21: :: AUTALG_1:21

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ is_transformable_to b₃ implies for b₄ being set holds
( b₄ in product (MSFuncs b₂,b₃) implies b₄ is ManySortedFunction of b₂,b₃ ) )

proof

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
assume E18: c₂ is_transformable_to c₃ ;
let c₄ be set ;
assume E19: c₄ in product (MSFuncs c₂,c₃) ;
set c₅ = MSFuncs c₂,c₃;
consider c₆ being Function such that
E20: ( c₄ = c₆ & dom c₆ = dom (MSFuncs c₂,c₃) & ( for b₁ being set holds
( b₁ in dom (MSFuncs c₂,c₃) implies c₆ . b₁ in (MSFuncs c₂,c₃) . b₁ ) ) ) by E19, CARD_3:def 5;
E21: ( dom (MSFuncs c₂,c₃) = c₁ & dom c₆ = c₁ ) by E20, PBOOLE:def 3;
E22: for b₁ being set holds
( b₁ in c₁ implies c₆ . b₁ in Funcs (c₂ . b₁),(c₃ . b₁) )

proof

let c₇ be set ;
assume E23: c₇ in c₁ ;
then (MSFuncs c₂,c₃) . c₇ = Funcs (c₂ . c₇),(c₃ . c₇) by PBOOLE:def 22;
hence c₆ . c₇ in Funcs (c₂ . c₇),(c₃ . c₇) by E20, E21, E23;

end;

E23: for b₁ being set holds
not ( b₁ in c₁ & ( for b₂ being Function holds
not ( b₂ = c₆ . b₁ & dom b₂ = c₂ . b₁ & rng b₂ c= c₃ . b₁ ) ) )

proof

let c₇ be set ;
assume c₇ in c₁ ;
then c₆ . c₇ in Funcs (c₂ . c₇),(c₃ . c₇) by E22;
hence ex b₁ being Function st
( b₁ = c₆ . c₇ & dom b₁ = c₂ . c₇ & rng b₁ c= c₃ . c₇ ) by FUNCT_2:def 2;

end;

E24: for b₁ being set holds
( b₁ in c₁ implies c₆ . b₁ is Function of c₂ . b₁,c₃ . b₁ )

proof

let c₇ be set ;
assume E25: c₇ in c₁ ;
then consider c₈ being Function such that
E26: ( c₈ = c₆ . c₇ & dom c₈ = c₂ . c₇ & rng c₈ c= c₃ . c₇ ) by E23;
( c₃ . c₇ = {} implies c₂ . c₇ = {} ) by E18, E25, PZFMISC1:def 3;
hence c₆ . c₇ is Function of c₂ . c₇,c₃ . c₇ by E26, FUNCT_2:def 1, RELSET_1:11;

end;

c₆ is ManySortedSet of c₁ by E21, PBOOLE:def 3;
hence c₄ is ManySortedFunction of c₂,c₃ by E20, E24, PBOOLE:def 18;

end;

theorem Th22: :: AUTALG_1:22

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ is_transformable_to b₃ implies for b₄ being ManySortedFunction of b₂,b₃ holds b₄ in product (MSFuncs b₂,b₃) )

proof

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
assume E19: c₂ is_transformable_to c₃ ;
let c₄ be ManySortedFunction of c₂,c₃;
set c₅ = MSFuncs c₂,c₃;
E20: ( dom c₄ = c₁ & dom (MSFuncs c₂,c₃) = c₁ ) by PBOOLE:def 3;

now

let c₆ be set ;
assume E21: c₆ in dom (MSFuncs c₂,c₃) ;
then reconsider c₇ = c₆ as Element of c₁ by PBOOLE:def 3;
E22: c₄ . c₇ is Function of c₂ . c₇,c₃ . c₇ by E20, E21, PBOOLE:def 18;
( c₃