set fs = the Element of the carrier of J;
set ps = the Element of the carrier of J;
set co = the FinSequence of the carrier' of J;
set qs = {1,2};
set qq = the Function of [:{1,2},(Union X):], the carrier' of J;
reconsider Q = AlgLangSignature(# the carrier of J, the carrier' of J, the Arity of J, the ResultSort of J, the Element of the carrier of J, the Element of the carrier of J, the FinSequence of the carrier' of J,{1,2}, the Function of [:{1,2},(Union X):], the carrier' of J #) as non empty non void AlgLangSignature over Union X ;
take Q ; :: thesis: Q is J -extension
thus J is Subsignature of Q by INSTALG1:13; :: according to AOFA_L00:def 2 :: thesis: verum