let f, g be 1-sorted ; :: thesis: Carr {f,g} = { the carrier of f, the carrier of g}

thus Carr {f,g} c= { the carrier of f, the carrier of g} :: according to XBOOLE_0:def 10 :: thesis: { the carrier of f, the carrier of g} c= Carr {f,g}

thus Carr {f,g} c= { the carrier of f, the carrier of g} :: according to XBOOLE_0:def 10 :: thesis: { the carrier of f, the carrier of g} c= Carr {f,g}

proof

thus
{ the carrier of f, the carrier of g} c= Carr {f,g}
:: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Carr {f,g} or a in { the carrier of f, the carrier of g} )

assume a in Carr {f,g} ; :: thesis: a in { the carrier of f, the carrier of g}

then consider s being 1-sorted such that

A1: s in {f,g} and

A2: a = the carrier of s by Def7;

end;assume a in Carr {f,g} ; :: thesis: a in { the carrier of f, the carrier of g}

then consider s being 1-sorted such that

A1: s in {f,g} and

A2: a = the carrier of s by Def7;

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { the carrier of f, the carrier of g} or a in Carr {f,g} )

A3: f in {f,g} by TARSKI:def 2;

A4: g in {f,g} by TARSKI:def 2;

assume A5: a in { the carrier of f, the carrier of g} ; :: thesis: a in Carr {f,g}

end;A3: f in {f,g} by TARSKI:def 2;

A4: g in {f,g} by TARSKI:def 2;

assume A5: a in { the carrier of f, the carrier of g} ; :: thesis: a in Carr {f,g}