let f, g be Function; :: thesis: for A being set holds <:f,g:> | A = <:f,(g | A):>
let A be set ; :: thesis: <:f,g:> | A = <:f,(g | A):>
thus <:f,g:> | A = (<:g,f:> ~ ) | A by Th6
.= (<:g,f:> | A) ~ by Th7
.= <:(g | A),f:> ~ by Th10
.= <:f,(g | A):> by Th6 ; :: thesis: verum