:: AMI_1 semantic presentation

theorem :: AMI_1:1

canceled;

theorem E1: :: AMI_1:2

for b₁, b₂ being set holds
1 <> [b₁,b₂] by ZFMISC_1:8, CARD_5:1;

theorem :: AMI_1:3

for b₁, b₂ being set holds
2 <> [b₁,b₂] by ZFMISC_1:10, CARD_5:1;

theorem :: AMI_1:4

canceled;

theorem E2: :: AMI_1:5

for b₁, b₂, b₃, b₄ being set holds
( b₁ <> b₂ implies product (b₁,b₂ --> {b₃},{b₄}) = {(b₁,b₂ --> b₃,b₄)} )

proof

let c₁, c₂, c₃, c₄ be set ;
assume E3: c₁ <> c₂ ;
set c₅ = {(c₁,c₂ --> c₃,c₄)};
set c₆ = c₁,c₂ --> {c₃},{c₄};
E4: dom (c₁,c₂ --> {c₃},{c₄}) = {c₁,c₂} by FUNCT_4:65;

now

let c₇ be set ;
thus not ( c₇ in {(c₁,c₂ --> c₃,c₄)} & ( for b₁ being Function holds
not ( c₇ = b₁ & dom b₁ = dom (c₁,c₂ --> {c₃},{c₄}) & ( for b₂ being set holds
( b₂ in dom (c₁,c₂ --> {c₃},{c₄}) implies b₁ . b₂ in (c₁,c₂ --> {c₃},{c₄}) . b₂ ) ) ) ) )

proof

assume E5: c₇ in {(c₁,c₂ --> c₃,c₄)} ;
take c₈ = c₁,c₂ --> c₃,c₄;
thus c₇ = c₈ by E5, TARSKI:def 1;
thus dom c₈ = dom (c₁,c₂ --> {c₃},{c₄}) by E4, FUNCT_4:65;
let c₉ be set ;
assume c₉ in dom (c₁,c₂ --> {c₃},{c₄}) ;
then E6: ( c₉ = c₁ or c₉ = c₂ ) by E4, TARSKI:def 2;
( c₈ . c₁ = c₃ & (c₁,c₂ --> {c₃},{c₄}) . c₁ = {c₃} & c₈ . c₂ = c₄ & (c₁,c₂ --> {c₃},{c₄}) . c₂ = {c₄} ) by E3, FUNCT_4:66;
hence c₈ . c₉ in (c₁,c₂ --> {c₃},{c₄}) . c₉ by E6, TARSKI:def 1;

end;

given c₈ being Function such that E5: c₇ = c₈ and
E6: dom c₈ = dom (c₁,c₂ --> {c₃},{c₄}) and
E7: for b₁ being set holds
( b₁ in dom (c₁,c₂ --> {c₃},{c₄}) implies c₈ . b₁ in (c₁,c₂ --> {c₃},{c₄}) . b₁ ) ;
( c₁ in dom (c₁,c₂ --> {c₃},{c₄}) & c₂ in dom (c₁,c₂ --> {c₃},{c₄}) ) by E4, TARSKI:def 2;
then ( c₈ . c₁ in (c₁,c₂ --> {c₃},{c₄}) . c₁ & c₈ . c₂ in (c₁,c₂ --> {c₃},{c₄}) . c₂ & (c₁,c₂ --> {c₃},{c₄}) . c₁ = {c₃} & (c₁,c₂ --> {c₃},{c₄}) . c₂ = {c₄} ) by E3, E7, FUNCT_4:66;
then ( c₈ . c₁ = c₃ & c₈ . c₂ = c₄ ) by TARSKI:def 1;
then c₈ = c₁,c₂ --> c₃,c₄ by E4, E6, FUNCT_4:69;
hence c₇ in {(c₁,c₂ --> c₃,c₄)} by E5, TARSKI:def 1;

end;

hence product (c₁,c₂ --> {c₃},{c₄}) = {(c₁,c₂ --> c₃,c₄)} by CARD_3:def 5;

end;

definition

let c₁ be set ;
attr a₂ is strict;
struct AMI-Struct of c₁ -> 1-sorted ;
aggr AMI-Struct(# carrier, Instruction-Counter, Instruction-Locations, Instruction-Codes, Instructions, Object-Kind, Execution #) -> AMI-Struct of a₁;
sel Instruction-Counter c₂ -> Element of the carrier of a₂;
sel Instruction-Locations c₂ -> Subset of the carrier of a₂;
sel Instruction-Codes c₂ -> non empty set ;
sel Instructions c₂ -> non empty Subset of [:the Instruction-Codes of a₂,(((union a₁) \/ the carrier of a₂) * ):];
sel Object-Kind c₂ -> Function of the carrier of a₂,a₁ \/ {the Instructions of a₂,the Instruction-Locations of a₂};
sel Execution c₂ -> Function of the Instructions of a₂, Funcs (product the Object-Kind of a₂),(product the Object-Kind of a₂);

end;

definition

let c₁ be set ;
canceled;
func Trivial-AMI c₁ -> strict AMI-Struct of a₁ means :E3: :: AMI_1:def 2
( the carrier of a₂ = {0,1} & the Instruction-Counter of a₂ = 0 & the Instruction-Locations of a₂ = {1} & the Instruction-Codes of a₂ = {0} & the Instructions of a₂ = {[0,{} ]} & the Object-Kind of a₂ = 0,1 --> {1},{[0,{} ]} & the Execution of a₂ = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) );
existence

proof

reconsider c₂ = 0 as Element of {0,1} by TARSKI:def 2;
( 0 in {0} & {} in ((union c₁) \/ {0,1}) * ) by FINSEQ_1:66, TARSKI:def 1;
then [0,{} ] in [:{0},(((union c₁) \/ {0,1}) * ):] by ZFMISC_1:106;
then reconsider c₃ = {[0,{} ]} as non empty Subset of [:{0},(((union c₁) \/ {0,1}) * ):] by ZFMISC_1:37;
reconsider c₄ = {1} as non empty Subset of {0,1} by ZFMISC_1:12;
set c₅ = 0,1 --> c₄,c₃;
( rng (0,1 --> c₄,c₃) c= {c₃,c₄} & {c₃,c₄} c= c₁ \/ {c₃,c₄} ) by FUNCT_4:65, XBOOLE_1:7;
then ( dom (0,1 --> c₄,c₃) = {0,1} & rng (0,1 --> c₄,c₃) c= c₁ \/ {c₃,c₄} ) by FUNCT_4:65, XBOOLE_1:1;
then reconsider c₆ = 0,1 --> c₄,c₃ as Function of {0,1},c₁ \/ {c₃,c₄} by FUNCT_2:def 1, RELSET_1:11;
id (product c₆) in Funcs (product c₆),(product c₆) by FUNCT_2:12;
then reconsider c₇ = c₃ --> (id (product c₆)) as Function of c₃, Funcs (product c₆),(product c₆) by FUNCOP_1:57;
take AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) ;
thus ( the carrier of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = {0,1} & the Instruction-Counter of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = 0 & the Instruction-Locations of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = {1} & the Instruction-Codes of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = {0} & the Instructions of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = {[0,{} ]} & the Object-Kind of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = 0,1 --> {1},{[0,{} ]} & the Execution of AMI-Struct(# {0,1},c₂,c₄,{0},c₃,c₆,c₇ #) = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) ) ;

end;

uniqueness ;

end;

:: deftheorem AMI_1:def 1 :

:: deftheorem E3 defines Trivial-AMI AMI_1:def 2 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is void means :E4: :: AMI_1:def 3
the Instruction-Locations of a₂ is empty;

end;

:: deftheorem E4 defines void AMI_1:def 3 :

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void ;
coherence

proof

thus not the carrier of (Trivial-AMI c₁) is empty by E3; :: according to STRUCT_0:def 1
thus not the Instruction-Locations of (Trivial-AMI c₁) is empty by E3; :: according to AMI_1:def 3

end;

registration

let c₁ be set ;
cluster non empty non void AMI-Struct of a₁;
existence

proof

take Trivial-AMI c₁ ;
thus ( not Trivial-AMI c₁ is empty & not Trivial-AMI c₁ is void ) ;

end;

registration

let c₁ be set ;
let c₂ be non void AMI-Struct of c₁;
cluster the Instruction-Locations of a₂ -> non empty ;
coherence by E4;

end;

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
mode Object is Element of a₂;

end;

definition

let c₁ be set ;
let c₂ be non empty non void AMI-Struct of c₁;
mode Instruction-Location is Element of the Instruction-Locations of a₂;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
mode Instruction is Element of the Instructions of a₂;

end;

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
canceled;
func IC c₂ -> Object of a₂ equals :: AMI_1:def 5
the Instruction-Counter of a₂;
correctness ;

end;

:: deftheorem AMI_1:def 4 :

:: deftheorem defines IC AMI_1:def 5 :

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
let c₃ be Object of c₂;
func ObjectKind c₃ -> Element of a₁ \/ {the Instructions of a₂,the Instruction-Locations of a₂} equals :: AMI_1:def 6
the Object-Kind of a₂ . a₃;
correctness ;

end;

:: deftheorem defines ObjectKind AMI_1:def 6 :

registration

let c₁ be Function;
cluster product a₁ -> functional ;
coherence

proof

set c₂ = product c₁;
let c₃ be set ; :: according to FRAENKEL:def 1
assume c₃ in product c₁ ;
then ex b₁ being Function st
( c₃ = b₁ & dom b₁ = dom c₁ & ( for b₂ being set holds
( b₂ in dom c₁ implies b₁ . b₂ in c₁ . b₂ ) ) ) by CARD_3:def 5;
hence c₃ is Function ;

end;

registration

let c₁ be set ;
let c₂ be with_non-empty_elements set ;
let c₃ be Function of c₁,c₂;
cluster product a₃ -> non empty functional ;
coherence

proof

rng c₃ c= c₂ by RELSET_1:12;
then not {} in rng c₃ by SETFAM_1:def 9;
hence not product c₃ is empty by CARD_3:37;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
mode State is Element of product the Object-Kind of a₂;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Instruction of c₂;
let c₄ be State of c₂;
func Exec c₃,c₄ -> State of a₂ equals :: AMI_1:def 7
(the Execution of a₂ . a₃) . a₄;
coherence

proof

consider c₅ being Function such that
E5: ( the Execution of c₂ . c₃ = c₅ & dom c₅ = product the Object-Kind of c₂ & rng c₅ c= product the Object-Kind of c₂ ) by FUNCT_2:def 2;
(the Execution of c₂ . c₃) . c₄ in rng c₅ by E5, FUNCT_1:def 5;
hence (the Execution of c₂ . c₃) . c₄ is State of c₂ by E5;

end;

:: deftheorem defines Exec AMI_1:def 7 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is halting means :E5: :: AMI_1:def 8
for b₁ being State of a₂ holds Exec a₃,b₁ = b₁;

end;

:: deftheorem E5 defines halting AMI_1:def 8 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
attr a₂ is halting means :E6: :: AMI_1:def 9
ex b₁ being Instruction of a₂ st
( b₁ is halting & ( for b₂ being Instruction of a₂ holds
( b₂ is halting implies b₁ = b₂ ) ) );

end;

:: deftheorem E6 defines halting AMI_1:def 9 :

theorem E7: :: AMI_1:6

for b₁ being with_non-empty_elements set holds Trivial-AMI b₁ is halting

proof

let c₁ be with_non-empty_elements set ;
set c₂ = Trivial-AMI c₁;
E8: {[0,{} ]} = the Instructions of (Trivial-AMI c₁) by E3;
then reconsider c₃ = [0,{} ] as Instruction of (Trivial-AMI c₁) by TARSKI:def 1;
take c₃ ; :: according to AMI_1:def 9
thus c₃ is halting

proof

let c₄ be State of (Trivial-AMI c₁); :: according to AMI_1:def 8
E9: product the Object-Kind of (Trivial-AMI c₁) = product (0,1 --> {1},{[0,{} ]}) by E3
.= {(0,1 --> 1,[0,{} ])} by E2 ;
hence Exec c₃,c₄ = 0,1 --> 1,[0,{} ] by TARSKI:def 1
.= c₄ by E9, TARSKI:def 1 ;

end;

let c₄ be Instruction of (Trivial-AMI c₁);
assume c₄ is halting ;
thus c₃ = c₄ by E8, TARSKI:def 1;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster Trivial-AMI a₁ -> non empty strict non void halting ;
coherence by E7;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non void halting AMI-Struct of a₁;
existence

proof

take Trivial-AMI c₁ ;
thus Trivial-AMI c₁ is halting ;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
cluster halting Element of the Instructions of a₂;
existence

proof

ex b₁ being Instruction of c₂ st
( b₁ is halting & ( for b₂ being Instruction of c₂ holds
( b₂ is halting implies b₁ = b₂ ) ) ) by E6;
hence ex b₁ being Instruction of c₂ st b₁ is halting ;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
func halt c₂ -> Instruction of a₂ means :E8: :: AMI_1:def 10
a₃ is halting Instruction of a₂;
existence

proof

consider c₃ being Instruction of c₂ such that
E8: c₃ is halting and
for b₁ being Instruction of c₂ holds
( b₁ is halting implies c₃ = b₁ ) by E6;
take c₃ ;
thus c₃ is halting Instruction of c₂ by E8;

end;

uniqueness

proof

let c₃, c₄ be Instruction of c₂;
assume that
E8: c₃ is halting Instruction of c₂ and
E9: c₄ is halting Instruction of c₂ ;
consider c₅ being Instruction of c₂ such that
E10: ( c₅ is halting & ( for b₁ being Instruction of c₂ holds
( b₁ is halting implies c₅ = b₁ ) ) ) by E6;
c₅ = c₃ by E8, E10;
hence c₃ = c₄ by E9, E10;

end;

:: deftheorem E8 defines halt AMI_1:def 10 :

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
cluster halt a₂ -> halting ;
coherence by E8;

end;

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
attr a₂ is IC-Ins-separated means :E9: :: AMI_1:def 11
ObjectKind (IC a₂) = the Instruction-Locations of a₂;

end;

:: deftheorem E9 defines IC-Ins-separated AMI_1:def 11 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is data-oriented means :: AMI_1:def 12
the Object-Kind of a₂ " {the Instructions of a₂} c= the Instruction-Locations of a₂;

end;

:: deftheorem defines data-oriented AMI_1:def 12 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void AMI-Struct of c₁;
attr a₂ is steady-programmed means :E10: :: AMI_1:def 13
for b₁ being State of a₂
for b₂ being Instruction of a₂
for b₃ being Instruction-Location of a₂ holds (Exec b₂,b₁) . b₃ = b₁ . b₃;

end;

:: deftheorem E10 defines steady-programmed AMI_1:def 13 :

definition

let c₁ be set ;
let c₂ be non empty non void AMI-Struct of c₁;
attr a₂ is definite means :E11: :: AMI_1:def 14
for b₁ being Instruction-Location of a₂ holds ObjectKind b₁ = the Instructions of a₂;

end;

:: deftheorem E11 defines definite AMI_1:def 14 :

theorem E12: :: AMI_1:7

for b₁ being set holds Trivial-AMI b₁ is IC-Ins-separated

proof

let c₁ be set ;
E13: IC (Trivial-AMI c₁) = the Instruction-Counter of (Trivial-AMI c₁)
.= 0 by E3 ;
thus ObjectKind (IC (Trivial-AMI c₁)) = the Object-Kind of (Trivial-AMI c₁) . (IC (Trivial-AMI c₁))
.= (0,1 --> {1},{[0,{} ]}) . 0 by E13, E3
.= {1} by FUNCT_4:66
.= the Instruction-Locations of (Trivial-AMI c₁) by E3 ; :: according to AMI_1:def 11

end;

theorem E13: :: AMI_1:8

for b₁ being set holds Trivial-AMI b₁ is data-oriented

proof

let c₁ be set ;
let c₂ be set ; :: according to TARSKI:def 3,AMI_1:def 12
E14: 1 <> [0,{} ] by E1;
assume E15: c₂ in the Object-Kind of (Trivial-AMI c₁) " {the Instructions of (Trivial-AMI c₁)} ;
then ( c₂ in the carrier of (Trivial-AMI c₁) & the Object-Kind of (Trivial-AMI c₁) . c₂ in {the Instructions of (Trivial-AMI c₁)} ) by FUNCT_2:46;
then E16: the Object-Kind of (Trivial-AMI c₁) . c₂ = the Instructions of (Trivial-AMI c₁) by TARSKI:def 1
.= {[0,{} ]} by E3 ;
E17: the Object-Kind of (Trivial-AMI c₁) . 0 = (0,1 --> {1},{[0,{} ]}) . 0 by E3
.= {1} by FUNCT_4:66 ;
the carrier of (Trivial-AMI c₁) = {0,1} by E3;
then ( c₂ = 0 or c₂ = 1 ) by E15, TARSKI:def 2;
then c₂ in {1} by E14, E16, E17, TARSKI:def 1, ZFMISC_1:6;
hence c₂ in the Instruction-Locations of (Trivial-AMI c₁) by E3;

end;

theorem E14: :: AMI_1:9

for b₁ being set
for b₂, b₃ being State of (Trivial-AMI b₁) holds b₂ = b₃

proof

let c₁ be set ;
let c₂, c₃ be State of (Trivial-AMI c₁);
E15: product the Object-Kind of (Trivial-AMI c₁) = product (0,1 --> {1},{[0,{} ]}) by E3
.= {(0,1 --> 1,[0,{} ])} by E2 ;
hence c₂ = 0,1 --> 1,[0,{} ] by TARSKI:def 1
.= c₃ by E15, TARSKI:def 1 ;

end;

theorem E15: :: AMI_1:10

for b₁ being with_non-empty_elements set holds Trivial-AMI b₁ is steady-programmed

proof

let c₁ be with_non-empty_elements set ;
let c₂ be State of (Trivial-AMI c₁); :: according to AMI_1:def 13
let c₃ be Instruction of (Trivial-AMI c₁);
let c₄ be Instruction-Location of (Trivial-AMI c₁);
thus (Exec c₃,c₂) . c₄ = c₂ . c₄ by E14;

end;

theorem E16: :: AMI_1:11

for b₁ being set holds Trivial-AMI b₁ is definite

proof

let c₁ be set ;
let c₂ be Instruction-Location of (Trivial-AMI c₁); :: according to AMI_1:def 14
c₂ in the Instruction-Locations of (Trivial-AMI c₁) ;
then c₂ in {1} by E3;
then E17: c₂ = 1 by TARSKI:def 1;
thus ObjectKind c₂ = the Object-Kind of (Trivial-AMI c₁) . c₂
.= (0,1 --> {1},{[0,{} ]}) . 1 by E17, E3
.= {[0,{} ]} by FUNCT_4:66
.= the Instructions of (Trivial-AMI c₁) by E3 ;

end;

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void data-oriented ;
coherence by E13;

end;

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence by E12, E16;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster Trivial-AMI a₁ -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite ;
coherence by E15;

end;

registration

let c₁ be set ;
cluster strict data-oriented AMI-Struct of a₁;
existence

proof

take Trivial-AMI c₁ ;
thus ( Trivial-AMI c₁ is data-oriented & Trivial-AMI c₁ is strict ) ;

end;

registration

let c₁ be set ;
cluster non empty strict non void IC-Ins-separated data-oriented definite AMI-Struct of a₁;
existence

proof

take Trivial-AMI c₁ ;
thus ( Trivial-AMI c₁ is IC-Ins-separated & Trivial-AMI c₁ is data-oriented & Trivial-AMI c₁ is definite & Trivial-AMI c₁ is strict ) ;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite AMI-Struct of a₁;
existence

proof

take Trivial-AMI c₁ ;
thus ( Trivial-AMI c₁ is IC-Ins-separated & Trivial-AMI c₁ is data-oriented & Trivial-AMI c₁ is halting & Trivial-AMI c₁ is steady-programmed & Trivial-AMI c₁ is definite & Trivial-AMI c₁ is strict ) ;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated AMI-Struct of c₁;
let c₃ be State of c₂;
func IC c₃ -> Instruction-Location of a₂ equals :: AMI_1:def 15
a₃ . (IC a₂);
coherence

proof

dom the Object-Kind of c₂ = the carrier of c₂ by FUNCT_2:def 1;
then pi (product the Object-Kind of c₂),(IC c₂) = the Object-Kind of c₂ . (IC c₂) by CARD_3:22
.= ObjectKind (IC c₂)
.= the Instruction-Locations of c₂ by E9 ;
hence c₃ . (IC c₂) is Instruction-Location of c₂ by CARD_3:def 6;

end;

:: deftheorem defines IC AMI_1:def 15 :

theorem :: AMI_1:12

canceled;

theorem :: AMI_1:13

canceled;

theorem E17: :: AMI_1:14

for b₁, b₂, b₃ being set
for b₄, b₅ being Function holds
( ( b₄ tolerates b₅ & [b₁,b₂] in b₄ & [b₁,b₃] in b₅ ) implies ( b₂ = b₃ ) )

proof

let c₁, c₂, c₃ be set ;
let c₄, c₅ be Function;
assume c₄ tolerates c₅ ;
then consider c₆ being Function such that
E18: c₆ = c₄ \/ c₅ by PARTFUN1:130;
assume ( [c₁,c₂] in c₄ & [c₁,c₃] in c₅ ) ;
then ( [c₁,c₂] in c₆ & [c₁,c₃] in c₆ ) by E18, XBOOLE_0:def 2;
hence c₂ = c₃ by FUNCT_1:def 1;

end;

theorem E18: :: AMI_1:15

for b₁ being set holds
( ( ( for b₂ being set holds
( b₂ in b₁ implies b₂ is Function ) ) & ( for b₂, b₃ being Function holds
( ( b₂ in b₁ & b₃ in b₁ ) implies ( b₂ tolerates b₃ ) ) ) ) implies ( union b₁ is Function ) )

proof

let c₁ be set ;
assume that
E19: for b₁ being set holds
( b₁ in c₁ implies b₁ is Function ) and
E20: for b₁, b₂ being Function holds
( ( b₁ in c₁ & b₂ in c₁ ) implies ( b₁ tolerates b₂ ) ) ;

E21: now

let c₂ be set ;
assume c₂ in union c₁ ;
then consider c₃ being set such that
E22: ( c₂ in c₃ & c₃ in c₁ ) by TARSKI:def 4;
reconsider c₄ = c₃ as Function by E19, E22;
c₄ = c₄ ;
hence ex b₁, b₂ being set st [b₁,b₂] = c₂ by E22, RELAT_1:def 1;

end;

now

let c₂, c₃, c₄ be set ;
assume E22: ( [c₂,c₃] in union c₁ & [c₂,c₄] in union c₁ ) ;
then consider c₅ being set such that
E23: ( [c₂,c₃] in c₅ & c₅ in c₁ ) by TARSKI:def 4;
consider c₆ being set such that
E24: ( [c₂,c₄] in c₆ & c₆ in c₁ ) by E22, TARSKI:def 4;
reconsider c₇ = c₅, c₈ = c₆ as Function by E19, E23, E24;
c₇ tolerates c₈ by E20, E23, E24;
hence c₃ = c₄ by E23, E24, E17;

end;

hence union c₁ is Function by E21, FUNCT_1:def 1, RELAT_1:def 1;

end;

theorem :: AMI_1:16

canceled;

theorem :: AMI_1:17

canceled;

theorem E19: :: AMI_1:18

for b₁, b₂, b₃, b₄ being set holds b₁,b₂ --> b₃,b₄ = (b₁ .--> b₃) +* (b₂ .--> b₄) by FUNCT_4:def 4;

theorem E20: :: AMI_1:19

for b₁, b₂ being set holds b₁ .--> b₂ = {[b₁,b₂]}

proof

let c₁, c₂ be set ;
thus c₁ .--> c₂ = [:{c₁},{c₂}:] by FUNCOP_1:def 2
.= {[c₁,c₂]} by ZFMISC_1:35 ;

end;

theorem E21: :: AMI_1:20

for b₁, b₂, b₃ being set holds b₁,b₁ --> b₂,b₃ = b₁ .--> b₃

proof

let c₁, c₂, c₃ be set ;
E22: dom (c₁ .--> c₃) = {c₁} by FUNCOP_1:19
.= dom (