:: AMI_1 semantic presentation

theorem Th1: :: AMI_1:1
canceled;

theorem Th2: :: AMI_1:2
for b1, b2 being set holds
1 <> [b1,b2] by ZFMISC_1:8, CARD_5:1;

theorem Th3: :: AMI_1:3
for b1, b2 being set holds
2 <> [b1,b2] by ZFMISC_1:10, CARD_5:1;

theorem Th4: :: AMI_1:4
canceled;

theorem Th5: :: AMI_1:5
for b1, b2, b3, b4 being set holds
( b1 <> b2 implies product (b1,b2 --> {b3},{b4}) = {(b1,b2 --> b3,b4)} ) by CARD_3:63;

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

definition
let c1 be set ;
canceled;
func Trivial-AMI c1 -> strict AMI-Struct of a1 means :Def2: :: AMI_1:def 2
( the carrier of a2 = {0,1} & the Instruction-Counter of a2 = 0 & the Instruction-Locations of a2 = {1} & the Instruction-Codes of a2 = {0} & the Instructions of a2 = {[0,{} ]} & the Object-Kind of a2 = 0,1 --> {1},{[0,{} ]} & the Execution of a2 = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) );
existence
ex b1 being strict AMI-Struct of c1 st
( the carrier of b1 = {0,1} & the Instruction-Counter of b1 = 0 & the Instruction-Locations of b1 = {1} & the Instruction-Codes of b1 = {0} & the Instructions of b1 = {[0,{} ]} & the Object-Kind of b1 = 0,1 --> {1},{[0,{} ]} & the Execution of b1 = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) )
proof
reconsider c2 = 0 as Element of {0,1} by TARSKI:def 2;
( 0 in {0} & {} in ((union c1) \/ {0,1}) * ) by FINSEQ_1:66, TARSKI:def 1;
then [0,{} ] in [:{0},(((union c1) \/ {0,1}) * ):] by ZFMISC_1:106;
then reconsider c3 = {[0,{} ]} as non empty Subset of [:{0},(((union c1) \/ {0,1}) * ):] by ZFMISC_1:37;
reconsider c4 = {1} as non empty Subset of {0,1} by ZFMISC_1:12;
set c5 = 0,1 --> c4,c3;
( rng (0,1 --> c4,c3) c= {c3,c4} & {c3,c4} c= c1 \/ {c3,c4} ) by FUNCT_4:65, XBOOLE_1:7;
then ( dom (0,1 --> c4,c3) = {0,1} & rng (0,1 --> c4,c3) c= c1 \/ {c3,c4} ) by FUNCT_4:65, XBOOLE_1:1;
then reconsider c6 = 0,1 --> c4,c3 as Function of {0,1},c1 \/ {c3,c4} by FUNCT_2:def 1, RELSET_1:11;
id (product c6) in Funcs (product c6),(product c6) by FUNCT_2:12;
then reconsider c7 = c3 --> (id (product c6)) as Function of c3, Funcs (product c6),(product c6) by FUNCOP_1:57;
take AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) ;
thus ( the carrier of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = {0,1} & the Instruction-Counter of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = 0 & the Instruction-Locations of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = {1} & the Instruction-Codes of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = {0} & the Instructions of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = {[0,{} ]} & the Object-Kind of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = 0,1 --> {1},{[0,{} ]} & the Execution of AMI-Struct(# {0,1},c2,c4,{0},c3,c6,c7 #) = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) ) ;
end;
uniqueness
for b1, b2 being strict AMI-Struct of c1 holds
( the carrier of b1 = {0,1} & the Instruction-Counter of b1 = 0 & the Instruction-Locations of b1 = {1} & the Instruction-Codes of b1 = {0} & the Instructions of b1 = {[0,{} ]} & the Object-Kind of b1 = 0,1 --> {1},{[0,{} ]} & the Execution of b1 = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) & the carrier of b2 = {0,1} & the Instruction-Counter of b2 = 0 & the Instruction-Locations of b2 = {1} & the Instruction-Codes of b2 = {0} & the Instructions of b2 = {[0,{} ]} & the Object-Kind of b2 = 0,1 --> {1},{[0,{} ]} & the Execution of b2 = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) implies b1 = b2 ) ;
end;

:: deftheorem Def1 AMI_1:def 1 :
canceled;

:: deftheorem Def2 defines Trivial-AMI AMI_1:def 2 :
for b1 being set
for b2 being strict AMI-Struct of b1 holds
( b2 = Trivial-AMI b1 iff ( the carrier of b2 = {0,1} & the Instruction-Counter of b2 = 0 & the Instruction-Locations of b2 = {1} & the Instruction-Codes of b2 = {0} & the Instructions of b2 = {[0,{} ]} & the Object-Kind of b2 = 0,1 --> {1},{[0,{} ]} & the Execution of b2 = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) ) );

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
attr a2 is void means :Def3: :: AMI_1:def 3
the Instruction-Locations of a2 is empty;
end;

:: deftheorem Def3 defines void AMI_1:def 3 :
for b1 being set
for b2 being AMI-Struct of b1 holds
( b2 is void iff the Instruction-Locations of b2 is empty );

registration
let c1 be set ;
cluster Trivial-AMI a1 -> non empty strict non void ;
coherence
( not Trivial-AMI c1 is empty & not Trivial-AMI c1 is void )
proof
thus not the carrier of (Trivial-AMI c1) is empty by Def2; :: according to STRUCT_0:def 1
thus not the Instruction-Locations of (Trivial-AMI c1) is empty by Def2; :: according to AMI_1:def 3
end;
end;

registration
let c1 be set ;
cluster non empty non void AMI-Struct of a1;
existence
ex b1 being AMI-Struct of c1 st
( not b1 is empty & not b1 is void )
proof
take Trivial-AMI c1 ;
thus ( not Trivial-AMI c1 is empty & not Trivial-AMI c1 is void ) ;
end;
end;

registration
let c1 be set ;
let c2 be non void AMI-Struct of c1;
cluster the Instruction-Locations of a2 -> non empty ;
coherence
not the Instruction-Locations of c2 is empty by Def3;
end;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
mode Object is Element of a2;
end;

definition
let c1 be set ;
let c2 be non empty non void AMI-Struct of c1;
mode Instruction-Location is Element of the Instruction-Locations of a2;
end;

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
mode Instruction is Element of the Instructions of a2;
end;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
canceled;
func IC c2 -> Object of a2 equals :: AMI_1:def 5
the Instruction-Counter of a2;
correctness
coherence
the Instruction-Counter of c2 is Object of c2;
;
end;

:: deftheorem Def4 AMI_1:def 4 :
canceled;

:: deftheorem Def5 defines IC AMI_1:def 5 :
for b1 being set
for b2 being non empty AMI-Struct of b1 holds IC b2 = the Instruction-Counter of b2;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
let c3 be Object of c2;
func ObjectKind c3 -> Element of a1 \/ {the Instructions of a2,the Instruction-Locations of a2} equals :: AMI_1:def 6
the Object-Kind of a2 . a3;
correctness
coherence
the Object-Kind of c2 . c3 is Element of c1 \/ {the Instructions of c2,the Instruction-Locations of c2};
;
end;

:: deftheorem Def6 defines ObjectKind AMI_1:def 6 :
for b1 being set
for b2 being non empty AMI-Struct of b1
for b3 being Object of b2 holds ObjectKind b3 = the Object-Kind of b2 . b3;

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
mode State is Element of product the Object-Kind of a2;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be State of c2;
func Exec c3,c4 -> State of a2 equals :: AMI_1:def 7
(the Execution of a2 . a3) . a4;
coherence
(the Execution of c2 . c3) . c4 is State of c2
proof
consider c5 being Function such that
E3: ( the Execution of c2 . c3 = c5 & dom c5 = product the Object-Kind of c2 & rng c5 c= product the Object-Kind of c2 ) by FUNCT_2:def 2;
(the Execution of c2 . c3) . c4 in rng c5 by E3, FUNCT_1:def 5;
hence (the Execution of c2 . c3) . c4 is State of c2 by E3;
end;
end;

:: deftheorem Def7 defines Exec AMI_1:def 7 :
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1
for b3 being Instruction of b2
for b4 being State of b2 holds Exec b3,b4 = (the Execution of b2 . b3) . b4;

definition
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
let c3 be Instruction of c2;
attr a3 is halting means :Def8: :: AMI_1:def 8
for b1 being State of a2 holds Exec a3,b1 = b1;
end;

:: deftheorem Def8 defines halting AMI_1:def 8 :
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 is halting iff for b4 being State of b2 holds Exec b3,b4 = b4 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
attr a2 is halting means :Def9: :: AMI_1:def 9
ex b1 being Instruction of a2 st
( b1 is halting & ( for b2 being Instruction of a2 holds
( b2 is halting implies b1 = b2 ) ) );
end;

:: deftheorem Def9 defines halting AMI_1:def 9 :
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1 holds
( b2 is halting iff ex b3 being Instruction of b2 st
( b3 is halting & ( for b4 being Instruction of b2 holds
( b4 is halting implies b3 = b4 ) ) ) );

theorem Th6: :: AMI_1:6
for b1 being with_non-empty_elements set holds Trivial-AMI b1 is halting
proof
let c1 be with_non-empty_elements set ;
set c2 = Trivial-AMI c1;
E6: {[0,{} ]} = the Instructions of (Trivial-AMI c1) by Def2;
then reconsider c3 = [0,{} ] as Instruction of (Trivial-AMI c1) by TARSKI:def 1;
take c3 ; :: according to AMI_1:def 9
thus c3 is halting
proof
let c4 be State of (Trivial-AMI c1); :: according to AMI_1:def 8
E7: product the Object-Kind of (Trivial-AMI c1) = product (0,1 --> {1},{[0,{} ]}) by Def2
.= {(0,1 --> 1,[0,{} ])} by CARD_3:63 ;
hence Exec c3,c4 = 0,1 --> 1,[0,{} ] by TARSKI:def 1
.= c4 by E7, TARSKI:def 1 ;

end;
let c4 be Instruction of (Trivial-AMI c1);
assume c4 is halting ;
thus c3 = c4 by E6, TARSKI:def 1;
end;

registration
let c1 be with_non-empty_elements set ;
cluster Trivial-AMI a1 -> non empty strict non void halting ;
coherence
Trivial-AMI c1 is halting by Th6;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non void halting AMI-Struct of a1;
existence
ex b1 being non void AMI-Struct of c1 st b1 is halting
proof
take Trivial-AMI c1 ;
thus Trivial-AMI c1 is halting ;
end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non void halting AMI-Struct of c1;
cluster halting Element of the Instructions of a2;
existence
ex b1 being Instruction of c2 st b1 is halting
proof
ex b1 being Instruction of c2 st
( b1 is halting & ( for b2 being Instruction of c2 holds
( b2 is halting implies b1 = b2 ) ) ) by Def9;
hence ex b1 being Instruction of c2 st b1 is halting ;
end;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non void halting AMI-Struct of c1;
func halt c2 -> Instruction of a2 means :Def10: :: AMI_1:def 10
a3 is halting Instruction of a2;
existence
ex b1 being Instruction of c2 st
b1 is halting Instruction of c2
proof
consider c3 being Instruction of c2 such that
E6: c3 is halting and
for b1 being Instruction of c2 holds
( b1 is halting implies c3 = b1 ) by Def9;
take c3 ;
thus c3 is halting Instruction of c2 by E6;
end;
uniqueness
for b1, b2 being Instruction of c2 holds
( b1 is halting Instruction of c2 & b2 is halting Instruction of c2 implies b1 = b2 )
proof
let c3, c4 be Instruction of c2;
assume that
E6: c3 is halting Instruction of c2 and
E7: c4 is halting Instruction of c2 ;
consider c5 being Instruction of c2 such that
E8: ( c5 is halting & ( for b1 being Instruction of c2 holds
( b1 is halting implies c5 = b1 ) ) ) by Def9;
c5 = c3 by E6, E8;
hence c3 = c4 by E7, E8;
end;
end;

:: deftheorem Def10 defines halt AMI_1:def 10 :
for b1 being with_non-empty_elements set
for b2 being non void halting AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 = halt b2 iff b3 is halting Instruction of b2 );

registration
let c1 be with_non-empty_elements set ;
let c2 be non void halting AMI-Struct of c1;
cluster halt a2 -> halting ;
coherence
halt c2 is halting by Def10;
end;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
attr a2 is IC-Ins-separated means :Def11: :: AMI_1:def 11
 ObjectKind (IC a2) = the Instruction-Locations of a2;
end;

:: deftheorem Def11 defines IC-Ins-separated AMI_1:def 11 :
for b1 being set
for b2 being non empty AMI-Struct of b1 holds
( b2 is IC-Ins-separated iff ObjectKind (IC b2) = the Instruction-Locations of b2 );

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
attr a2 is data-oriented means :: AMI_1:def 12
the Object-Kind of a2 " {the Instructions of a2} c= the Instruction-Locations of a2;
end;

:: deftheorem Def12 defines data-oriented AMI_1:def 12 :
for b1 being set
for b2 being AMI-Struct of b1 holds
( b2 is data-oriented iff the Object-Kind of b2 " {the Instructions of b2} c= the Instruction-Locations of b2 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
attr a2 is steady-programmed means :Def13: :: AMI_1:def 13
for b1 being State of a2
for b2 being Instruction of a2
for b3 being Instruction-Location of a2 holds (Exec b2,b1) . b3 = b1 . b3;
end;

:: deftheorem Def13 defines steady-programmed AMI_1:def 13 :
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1 holds
( b2 is steady-programmed iff for b3 being State of b2
for b4 being Instruction of b2
for b5 being Instruction-Location of b2 holds (Exec b4,b3) . b5 = b3 . b5 );

definition
let c1 be set ;
let c2 be non empty non void AMI-Struct of c1;
attr a2 is definite means :Def14: :: AMI_1:def 14
for b1 being Instruction-Location of a2 holds ObjectKind b1 = the Instructions of a2;
end;

:: deftheorem Def14 defines definite AMI_1:def 14 :
for b1 being set
for b2 being non empty non void AMI-Struct of b1 holds
( b2 is definite iff for b3 being Instruction-Location of b2 holds ObjectKind b3 = the Instructions of b2 );

theorem Th7: :: AMI_1:7
for b1 being set holds Trivial-AMI b1 is IC-Ins-separated
proof
let c1 be set ;
E11: IC (Trivial-AMI c1) = the Instruction-Counter of (Trivial-AMI c1)
.= 0 by Def2 ;
thus ObjectKind (IC (Trivial-AMI c1)) = the Object-Kind of (Trivial-AMI c1) . (IC (Trivial-AMI c1))
.= (0,1 --> {1},{[0,{} ]}) . 0 by E11, Def2
.= {1} by FUNCT_4:66
.= the Instruction-Locations of (Trivial-AMI c1) by Def2 ; :: according to AMI_1:def 11
end;

theorem Th8: :: AMI_1:8
for b1 being set holds Trivial-AMI b1 is data-oriented
proof
let c1 be set ;
let c2 be set ; :: according to TARSKI:def 3,AMI_1:def 12
E12: 1 <> [0,{} ] by ZFMISC_1:8, CARD_5:1;
assume E13: c2 in the Object-Kind of (Trivial-AMI c1) " {the Instructions of (Trivial-AMI c1)} ;
then ( c2 in the carrier of (Trivial-AMI c1) & the Object-Kind of (Trivial-AMI c1) . c2 in {the Instructions of (Trivial-AMI c1)} ) by FUNCT_2:46;
then E14: the Object-Kind of (Trivial-AMI c1) . c2 = the Instructions of (Trivial-AMI c1) by TARSKI:def 1
.= {[0,{} ]} by Def2 ;
E15: the Object-Kind of (Trivial-AMI c1) . 0 = (0,1 --> {1},{[0,{} ]}) . 0 by Def2
.= {1} by FUNCT_4:66 ;
the carrier of (Trivial-AMI c1) = {0,1} by Def2;
then ( c2 = 0 or c2 = 1 ) by E13, TARSKI:def 2;
then c2 in {1} by E12, E14, E15, TARSKI:def 1, ZFMISC_1:6;
hence c2 in the Instruction-Locations of (Trivial-AMI c1) by Def2;
end;

theorem Th9: :: AMI_1:9
for b1 being set
for b2, b3 being State of (Trivial-AMI b1) holds b2 = b3
proof
let c1 be set ;
let c2, c3 be State of (Trivial-AMI c1);
E13: product the Object-Kind of (Trivial-AMI c1) = product (0,1 --> {1},{[0,{} ]}) by Def2
.= {(0,1 --> 1,[0,{} ])} by CARD_3:63 ;
hence c2 = 0,1 --> 1,[0,{} ] by TARSKI:def 1
.= c3 by E13, TARSKI:def 1 ;

end;

theorem Th10: :: AMI_1:10
for b1 being with_non-empty_elements set holds Trivial-AMI b1 is steady-programmed
proof
let c1 be with_non-empty_elements set ;
let c2 be State of (Trivial-AMI c1); :: according to AMI_1:def 13
let c3 be Instruction of (Trivial-AMI c1);
let c4 be Instruction-Location of (Trivial-AMI c1);
thus (Exec c3,c2) . c4 = c2 . c4 by Th9;
end;

theorem Th11: :: AMI_1:11
for b1 being set holds Trivial-AMI b1 is definite
proof
let c1 be set ;
let c2 be Instruction-Location of (Trivial-AMI c1); :: according to AMI_1:def 14
c2 in the Instruction-Locations of (Trivial-AMI c1) ;
then c2 in {1} by Def2;
then E15: c2 = 1 by TARSKI:def 1;
thus ObjectKind c2 = the Object-Kind of (Trivial-AMI c1) . c2
.= (0,1 --> {1},{[0,{} ]}) . 1 by E15, Def2
.= {[0,{} ]} by FUNCT_4:66
.= the Instructions of (Trivial-AMI c1) by Def2 ;
end;

registration
let c1 be set ;
cluster Trivial-AMI a1 -> non empty strict non void data-oriented ;
coherence
Trivial-AMI c1 is data-oriented by Th8;
end;

registration
let c1 be set ;
cluster Trivial-AMI a1 -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence
( Trivial-AMI c1 is IC-Ins-separated & Trivial-AMI c1 is definite ) by Th7, Th11;
end;

registration
let c1 be with_non-empty_elements set ;
cluster Trivial-AMI a1 -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite ;
coherence
Trivial-AMI c1 is steady-programmed by Th10;
end;

registration
let c1 be set ;
cluster strict data-oriented AMI-Struct of a1;
existence
ex b1 being AMI-Struct of c1 st
( b1 is data-oriented & b1 is strict )
proof
take Trivial-AMI c1 ;
thus ( Trivial-AMI c1 is data-oriented & Trivial-AMI c1 is strict ) ;
end;
end;

registration
let c1 be set ;
cluster non empty strict non void IC-Ins-separated data-oriented definite AMI-Struct of a1;
existence
ex b1 being non empty non void AMI-Struct of c1 st
( b1 is IC-Ins-separated & b1 is data-oriented & b1 is definite & b1 is strict )
proof
take Trivial-AMI c1 ;
thus ( Trivial-AMI c1 is IC-Ins-separated & Trivial-AMI c1 is data-oriented & Trivial-AMI c1 is definite & Trivial-AMI c1 is strict ) ;
end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite AMI-Struct of a1;
existence
ex b1 being non empty non void AMI-Struct of c1 st
( b1 is IC-Ins-separated & b1 is data-oriented & b1 is halting & b1 is steady-programmed & b1 is definite & b1 is strict )
proof
take Trivial-AMI c1 ;
thus ( Trivial-AMI c1 is IC-Ins-separated & Trivial-AMI c1 is data-oriented & Trivial-AMI c1 is halting & Trivial-AMI c1 is steady-programmed & Trivial-AMI c1 is definite & Trivial-AMI c1 is strict ) ;
end;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated AMI-Struct of c1;
let c3 be State of c2;
func IC c3 -> Instruction-Location of a2 equals :: AMI_1:def 15
a3 . (IC a2);
coherence
c3 . (IC c2) is Instruction-Location of c2
proof
dom the Object-Kind of c2 = the carrier of c2 by FUNCT_2:def 1;
then pi (product the Object-Kind of c2),(IC c2) = the Object-Kind of c2 . (IC c2) by CARD_3:22
.= ObjectKind (IC c2)
.= the Instruction-Locations of c2 by Def11 ;
hence c3 . (IC c2) is Instruction-Location of c2 by CARD_3:def 6;
end;
end;

:: deftheorem Def15 defines IC AMI_1:def 15 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated AMI-Struct of b1
for b3 being State of b2 holds IC b3 = b3 . (IC b2);

theorem Th12: :: AMI_1:12
canceled;

theorem Th13: :: AMI_1:13
canceled;

theorem Th14: :: AMI_1:14
for b1, b2, b3 being set
for b4, b5 being Function holds
( b4 tolerates b5 & [b1,b2] in b4 & [b1,b3] in b5 implies b2 = b3 )
proof
let c1, c2, c3 be set ;
let c4, c5 be Function;
assume c4 tolerates c5 ;
then consider c6 being Function such that
E16: c6 = c4 \/ c5 by PARTFUN1:130;
assume ( [c1,c2] in c4 & [c1,c3] in c5 ) ;
then ( [c1,c2] in c6 & [c1,c3] in c6 ) by E16, XBOOLE_0:def 2;
hence c2 = c3 by FUNCT_1:def 1;
end;

theorem Th15: :: AMI_1:15
for b1 being set holds
( ( for b2 being set holds
( b2 in b1 implies b2 is Function ) ) & ( for b2, b3 being Function holds
( b2 in b1 & b3 in b1 implies b2 tolerates b3 ) ) implies union b1 is Function )
proof
let c1 be set ;
assume that
E17: for b1 being set holds
( b1 in c1 implies b1 is Function ) and
E18: for b1, b2 being Function holds
( b1 in c1 & b2 in c1 implies b1 tolerates b2 ) ;
E19: now
let c2 be set ;
assume c2 in union c1 ;
then consider c3 being set such that
E20: ( c2 in c3 & c3 in c1 ) by TARSKI:def 4;
reconsider c4 = c3 as Function by E17, E20;
c4 = c4 ;
hence ex b1, b2 being set st [b1,b2] = c2 by E20, RELAT_1:def 1;
end;
now
let c2, c3, c4 be set ;
assume E20: ( [c2,c3] in union c1 & [c2,c4] in union c1 ) ;
then consider c5 being set such that
E21: ( [c2,c3] in c5 & c5 in c1 ) by TARSKI:def 4;
consider c6 being set such that
E22: ( [c2,c4] in c6 & c6 in c1 ) by E20, TARSKI:def 4;
reconsider c7 = c5, c8 = c6 as Function by E17, E21, E22;
c7 tolerates c8 by E18, E21, E22;
hence c3 = c4 by E21, E22, Th14;
end;
hence union c1 is Function by E19, FUNCT_1:def 1, RELAT_1:def 1;
end;

theorem Th16: :: AMI_1:16
canceled;

theorem Th17: :: AMI_1:17
canceled;

theorem Th18: :: AMI_1:18
for b1, b2, b3, b4 being set holds b1,b2 --> b3,b4 = (b1 .--> b3) +* (b2 .--> b4) by FUNCT_4:def 4;

theorem Th19: :: AMI_1:19
for b1, b2 being set holds b1 .--> b2 = {[b1,b2]} by CQC_LANG:45;

theorem Th20: :: AMI_1:20
for b1, b2, b3 being set holds b1,b1 --> b2,b3 = b1 .--> b3 by CQC_LANG:44;

theorem Th21: :: AMI_1:21
canceled;

theorem Th22: :: AMI_1:22
for b1 being set
for b2 being Function holds
( b1 in product b2 implies b1 is Function ) by CARD_3:64;

definition
let c1 be Function;
func sproduct c1 -> set means :Def16: :: AMI_1:def 16
for b1 being set holds
( b1 in a2 iff ex b2 being Function st
( b1 = b2 & dom b2 c= dom a1 & ( for b3 being set holds
( b3 in dom b2 implies b2 . b3 in a1 . b3 ) ) ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being Function st
( b2 = b3 & dom b3 c= dom c1 & ( for b4 being set holds
( b4 in dom b3 implies b3 . b4 in c1 . b4 ) ) ) )
proof
defpred S1[ set ] means ex b1 being Function st
( a1 = b1 & dom b1 c= dom c1 & ( for b2 being set holds
( b2 in dom b1 implies b1 . b2 in c1 . b2 ) ) );
consider c2 being set such that
E19: for b1 being set holds
( b1 in c2 iff ( b1 in PFuncs (dom c1),(union (rng c1)) & S1[b1] ) ) from XBOOLE_0:sch 1();
now
let c3 be set ;
thus not ( c3 in c2 & ( for b1 being Function holds
not ( c3 = b1 & dom b1 c= dom c1 & ( for b2 being set holds
( b2 in dom b1 implies b1 . b2 in c1 . b2 ) ) ) ) ) by E19;
given c4 being Function such that E20: ( c3 = c4 & dom c4 c= dom c1 & ( for b1 being set holds
( b1 in dom c4 implies c4 . b1 in c1 . b1 ) ) ) ;
rng c4 c= union (rng c1)
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in rng c4 ;
then consider c6 being set such that
E21: ( c6 in dom c4 & c5 = c4 . c6 ) by FUNCT_1:def 5;
E22: c4 . c6 in c1 . c6 by E20, E21;
c1 . c6 in rng c1 by E20, E21, FUNCT_1:def 5;
hence c5 in union (rng c1) by E21, E22, TARSKI:def 4;
end;
then c3 in PFuncs (dom c1),(union (rng c1)) by E20, PARTFUN1:def 5;
hence c3 in c2 by E19, E20;
end;
hence ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being Function st
( b2 = b3 & dom b3 c= dom c1 & ( for b4 being set holds
( b4 in dom b3 implies b3 . b4 in c1 . b4 ) ) ) ) ;
end;
uniqueness
for b1, b2 being set holds
( ( for b3 being set holds
( b3 in b1 iff ex b4 being Function st
( b3 = b4 & dom b4 c= dom c1 & ( for b5 being set holds
( b5 in dom b4 implies b4 . b5 in c1 . b5 ) ) ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being Function st
( b3 = b4 & dom b4 c= dom c1 & ( for b5 being set holds
( b5 in dom b4 implies b4 . b5 in c1 . b5 ) ) ) ) ) implies b1 = b2 )
proof
defpred S1[ set ] means ex b1 being Function st
( a1 = b1 & dom b1 c= dom c1 & ( for b2 being set holds
( b2 in dom b1 implies b1 . b2 in c1 . b2 ) ) );
let c2, c3 be set ;
assume that
E19: for b1 being set holds
( b1 in c2 iff S1[b1] ) and