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 a', b', c' being object of C2 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 C2
for a', b', c' being object of C1 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 C1
for a', b', c' being object of C2 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 C2
for a', b', c' being object of C1 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 C2
for a', b', c' being object of C1 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 C2
for a', b', c' being object of C1 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 C2; :: thesis: for a', b', c' being object of C1 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 C1; :: thesis: ( a' = a & b' = b & c' = c implies the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a) )
assume ( a' = a & b' = b & c' = c ) ; :: thesis: the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a)
then A4: the Comp of C2 . c,b,a = ~ (the Comp of C1 . a',b',c') by A3;
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 A4, FUNCT_4:53; :: thesis: verum