let A, B be Category; :: thesis: IdCat [:A,B:] = [:(IdCat A),(IdCat B):]

now :: thesis: ( [: the carrier of (IdCat A), the carrier of (IdCat B):] = the carrier of (IdCat [:A,B:]) & the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] & [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )

reconsider OA = the carrier of (IdCat A) as non empty Subset of the carrier of A by CAT_2:def 4;
set AB = { (id c) where c is Object of [:A,B:] : verum } ;
set MA = { (id a) where a is Object of A : verum } ;
set MB = { (id b) where b is Object of B : verum } ;
A1: { (id c) where c is Object of [:A,B:] : verum } = [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]

proof

thus { (id c) where c is Object of [:A,B:] : verum } c= [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] :: according to XBOOLE_0:def 10 :: thesis: [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] c= { (id c) where c is Object of [:A,B:] : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (id c) where c is Object of [:A,B:] : verum } or x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] )
assume x in { (id c) where c is Object of [:A,B:] : verum } ; :: thesis: x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
then consider c being Object of [:A,B:] such that
A2: x = id c ;
consider c1 being Object of A, c2 being Object of B such that
A3: c = [c1,c2] by DOMAIN_1:1;
A4: id c2 in { (id b) where b is Object of B : verum } ;
A5: id c1 in { (id a) where a is Object of A : verum } ;
id c = [(id c1),(id c2)] by A3, CAT_2:31;
hence x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] by A2, A5, A4, ZFMISC_1:87; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] or x in { (id c) where c is Object of [:A,B:] : verum } )
assume x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] ; :: thesis: x in { (id c) where c is Object of [:A,B:] : verum }
then consider x1, x2 being object such that
A6: x1 in { (id a) where a is Object of A : verum } and
A7: x2 in { (id b) where b is Object of B : verum } and
A8: x = [x1,x2] by ZFMISC_1:84;
consider a being Object of A such that
A9: x1 = id a by A6;
consider b being Object of B such that
A10: x2 = id b by A7;
id [a,b] = [(id a),(id b)] by CAT_2:31;
hence x in { (id c) where c is Object of [:A,B:] : verum } by A8, A9, A10; :: thesis: verum

end;

reconsider OB = the carrier of (IdCat B) as non empty Subset of the carrier of B by CAT_2:def 4;
reconsider MB = the carrier' of (IdCat B) as non empty Subset of the carrier' of B by CAT_2:7;
reconsider MA = the carrier' of (IdCat A) as non empty Subset of the carrier' of A by CAT_2:7;
A11: the carrier of (IdCat B) = the carrier of B by Def20;
the carrier of (IdCat A) = the carrier of A by Def20;
hence [: the carrier of (IdCat A), the carrier of (IdCat B):] = the carrier of (IdCat [:A,B:]) by A11, Def20; :: thesis: ( the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] & [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
A12: the Target of (IdCat B) = the Target of B | the carrier' of (IdCat B) by Th4;
A13: the Source of (IdCat B) = the Source of B | the carrier' of (IdCat B) by Th4;
A14: the carrier' of (IdCat B) = { (id b) where b is Object of B : verum } by Def20;
the carrier' of (IdCat A) = { (id a) where a is Object of A : verum } by Def20;
hence A15: the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] by A1, A14, Def20; :: thesis: ( [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
the Source of (IdCat A) = the Source of A | the carrier' of (IdCat A) by Th4;
hence [: the Source of (IdCat A), the Source of (IdCat B):] = [: the Source of A, the Source of B:] | [:MA,MB:] by A13, FUNCT_3:81
.= the Source of (IdCat [:A,B:]) by A15, Th4 ;
:: thesis: ( [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
the Target of (IdCat A) = the Target of A | the carrier' of (IdCat A) by Th4;
hence [: the Target of (IdCat A), the Target of (IdCat B):] = [: the Target of A, the Target of B:] | [:MA,MB:] by A12, FUNCT_3:81
.= the Target of (IdCat [:A,B:]) by A15, Th4 ;
:: thesis: |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:])
A16: the Comp of (IdCat A) = the Comp of A || MA by Th4;
the Comp of (IdCat B) = the Comp of B || MB by Th4;
hence |: the Comp of (IdCat A), the Comp of (IdCat B):| = |: the Comp of A, the Comp of B:| || [:MA,MB:] by A16, FUNCT_4:126
.= the Comp of (IdCat [:A,B:]) by A15, Th4 ;
:: thesis: verum

end;

hence IdCat [:A,B:] = [:(IdCat A),(IdCat B):] ; :: thesis: verum