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 Th2
.= (<:g,f:> | A) ~ by Th3
.= <:(g | A),f:> ~ by Th5
.= <:f,(g | A):> by Th2 ; :: thesis: verum