let X1, X2 be StackAlgebra; :: thesis: ( ex F, G being Function st F,G form_isomorphism_between X1,X2 implies ex F, G being Function st F,G form_isomorphism_between X2,X1 )
given F, G being Function such that A1: F,G form_isomorphism_between X1,X2 ; :: thesis: ex F, G being Function st F,G form_isomorphism_between X2,X1
take F " ; :: thesis: ex G being Function st F " ,G form_isomorphism_between X2,X1
take G " ; :: thesis: F " ,G " form_isomorphism_between X2,X1
thus F " ,G " form_isomorphism_between X2,X1 by A1, Th43; :: thesis: verum