let C1, C2 be non empty AltCatStr ; :: thesis: ( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) implies ( the carrier of C1 = the carrier of C2 & the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being Object of C2
for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) ) )
assume that
A1: the carrier of C2 = the carrier of C1 and
A2: the Arrows of C2 = ~ the Arrows of C1 and
A3: for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ; :: thesis: ( the carrier of C1 = the carrier of C2 & the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being Object of C2
for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) )
thus the carrier of C1 = the carrier of C2 by A1; :: thesis: ( the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being Object of C2
for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) )
dom the Arrows of C1 = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def 2;
hence the Arrows of C1 = ~ the Arrows of C2 by A2, FUNCT_4:52; :: thesis: for a, b, c being Object of C2
for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a))
let a, b, c be Object of C2; :: thesis: for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a))
let a9, b9, c9 be Object of C1; :: thesis: ( a9 = a & b9 = b & c9 = c implies the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) )
assume that
A4: a9 = a and
A5: b9 = b and
A6: c9 = c ; :: thesis: the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a))
A7: the Comp of C2 . (c,b,a) = ~ ( the Comp of C1 . (a9,b9,c9)) by A3, A4, A5, A6;
dom ( the Comp of C1 . (a9,b9,c9)) c= [:( the Arrows of C1 . (b9,c9)),( the Arrows of C1 . (a9,b9)):] ;
hence the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) by A7, FUNCT_4:52; :: thesis: verum