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
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (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
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (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
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (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
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (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
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a) ) )
dom the Arrows of C1 = [:the carrier of C1,the carrier of C1:] by PARTFUN1:def 4;
hence the Arrows of C1 = ~ the Arrows of C2 by A2, FUNCT_4:53; :: thesis: for a, b, c being object of
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a)
let a, b, c be object of ; :: thesis: for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a)
let a', b', c' be object of ; :: thesis: ( a' = a & b' = b & c' = c implies the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a) )
assume that
A4: a' = a and
A5: b' = b and
A6: c' = c ; :: thesis: the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a)
A7: the Comp of C2 . c,b,a = ~ (the Comp of C1 . a',b',c') by A3, A4, A5, A6;
dom (the Comp of C1 . a',b',c') c= [:(the Arrows of C1 . b',c'),(the Arrows of C1 . a',b'):] ;
hence the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a) by A7, FUNCT_4:53; :: thesis: verum