let x, y, z, t be Surreal; :: thesis: comp ({z},x,y,{t}) = {(((z * y) + (x * t)) - (z * t))}
A1: comp ({z},x,y,{t}) c= {(((z * y) + (x * t)) - (z * t))}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in comp ({z},x,y,{t}) or o in {(((z * y) + (x * t)) - (z * t))} )
assume o in comp ({z},x,y,{t}) ; :: thesis: o in {(((z * y) + (x * t)) - (z * t))}
then consider x1, y1 being Surreal such that
A2: ( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in {z} & y1 in {t} ) by Def15;
( x1 = z & y1 = t ) by A2, TARSKI:def 1;
hence o in {(((z * y) + (x * t)) - (z * t))} by A2, TARSKI:def 1; :: thesis: verum

end;

( z in {z} & t in {t} ) by TARSKI:def 1;
then ((z * y) + (x * t)) - (z * t) in comp ({z},x,y,{t}) by Def15;
hence comp ({z},x,y,{t}) = {(((z * y) + (x * t)) - (z * t))} by A1, ZFMISC_1:33; :: thesis: verum