let C1, C2 be strict AltCatStr ; :: thesis: ( the carrier of C1 = F_{1}() & ( for i, j being Element of F_{1}() holds

( the Arrows of C1 . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C1 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) ) ) & the carrier of C2 = F_{1}() & ( for i, j being Element of F_{1}() holds

( the Arrows of C2 . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C2 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) ) ) implies C1 = C2 )

assume that

A1: the carrier of C1 = F_{1}()
and

A2: for i, j being Element of F_{1}() holds

( the Arrows of C1 . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C1 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) )
and

A3: the carrier of C2 = F_{1}()
and

A4: for i, j being Element of F_{1}() holds

( the Arrows of C2 . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C2 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) )
; :: thesis: C1 = C2

hence C1 = C2 by A1, A3, A5, ALTCAT_1:8; :: thesis: verum

( the Arrows of C1 . (i,j) = F

( the Arrows of C2 . (i,j) = F

assume that

A1: the carrier of C1 = F

A2: for i, j being Element of F

( the Arrows of C1 . (i,j) = F

A3: the carrier of C2 = F

A4: for i, j being Element of F

( the Arrows of C2 . (i,j) = F

A5: now :: thesis: for i, j, k being object st i in F_{1}() & j in F_{1}() & k in F_{1}() holds

the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)

the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)

let i, j, k be object ; :: thesis: ( i in F_{1}() & j in F_{1}() & k in F_{1}() implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) )

assume A6: ( i in F_{1}() & j in F_{1}() & k in F_{1}() )
; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)

hence the Comp of C1 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k))
by A2

.= the Comp of C2 . (i,j,k) by A4, A6 ;

:: thesis: verum

end;assume A6: ( i in F

hence the Comp of C1 . (i,j,k) = FuncComp (F

.= the Comp of C2 . (i,j,k) by A4, A6 ;

:: thesis: verum

now :: thesis: for i, j being Element of F_{1}() holds the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)

then
the Arrows of C1 = the Arrows of C2
by A1, A3, ALTCAT_1:7;let i, j be Element of F_{1}(); :: thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)

thus the Arrows of C1 . (i,j) = F_{2}(i,j)
by A2

.= the Arrows of C2 . (i,j) by A4 ; :: thesis: verum

end;thus the Arrows of C1 . (i,j) = F

.= the Arrows of C2 . (i,j) by A4 ; :: thesis: verum

hence C1 = C2 by A1, A3, A5, ALTCAT_1:8; :: thesis: verum