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 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 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:53; :: thesis: verum