Step |
Hyp |
Ref |
Expression |
1 |
|
s2co.1 |
|- ( ph -> F : X --> Y ) |
2 |
|
s2co.2 |
|- ( ph -> A e. X ) |
3 |
|
s2co.3 |
|- ( ph -> B e. X ) |
4 |
|
s3co.4 |
|- ( ph -> C e. X ) |
5 |
|
df-s3 |
|- <" A B C "> = ( <" A B "> ++ <" C "> ) |
6 |
2 3
|
s2cld |
|- ( ph -> <" A B "> e. Word X ) |
7 |
1 2 3
|
s2co |
|- ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> ) |
8 |
|
df-s3 |
|- <" ( F ` A ) ( F ` B ) ( F ` C ) "> = ( <" ( F ` A ) ( F ` B ) "> ++ <" ( F ` C ) "> ) |
9 |
5 6 4 1 7 8
|
cats1co |
|- ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> ) |