let C be initialized ConstructorSignature; :: thesis: for T being quasi-type of C
for a, b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T)
let T be quasi-type of C; :: thesis: for a, b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T)
let a, b be quasi-adjective of C; :: thesis: a ast (b ast T) = b ast (a ast T)
thus a ast (b ast T) = [({a} \/ ({b} \/ (adjs T))),(the_base_of (b ast T))] by MCART_1:7
.= [({b} \/ ({a} \/ (adjs T))),(the_base_of (b ast T))] by XBOOLE_1:4
.= [({b} \/ ({a} \/ (adjs T))),(the_base_of T)] by MCART_1:7
.= [({b} \/ (adjs (a ast T))),(the_base_of T)] by MCART_1:7
.= b ast (a ast T) by MCART_1:7 ; :: thesis: verum