let X be StackAlgebra; :: thesis: ex F, G being Function st F,G form_isomorphism_between X,X
take F = id the carrier of X; :: thesis: ex G being Function st F,G form_isomorphism_between X,X
take G = id the carrier' of X; :: thesis: F,G form_isomorphism_between X,X
thus F,G form_isomorphism_between X,X ; :: thesis: verum